nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | help
less more | (0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip

merge
2010-02-01, by Cezary Kaliszyk
More proofs in the LF example.
2010-02-01, by Cezary Kaliszyk
merged
2010-02-01, by Christian Urban
slight tuning
2010-02-01, by Christian Urban
renamed function according to the name of the constant
2010-02-01, by Christian Urban
fixed problem with Bex1_rel renaming
2010-02-01, by Christian Urban
Ported LF to the generic lambda and solved the simpler _supp cases.
2010-02-01, by Cezary Kaliszyk
merged
2010-01-30, by Christian Urban
introduced a generic alpha (but not sure whether it is helpful)
2010-01-30, by Christian Urban
More in the LF example in the new nominal way, all is clear until support.
2010-01-29, by Cezary Kaliszyk
Fixed the induction problem + some more proofs.
2010-01-29, by Cezary Kaliszyk
equivariance of rfv and alpha.
2010-01-29, by Cezary Kaliszyk
Added the experiments with fun and function.
2010-01-29, by Cezary Kaliszyk
now also final step is proved - the supp of lambdas is now completely characterised
2010-01-29, by Christian Urban
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms
2010-01-29, by Christian Urban
improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
2010-01-28, by Christian Urban
merged
2010-01-28, by Christian Urban
general abstraction operator and complete characterisation of its support and freshness
2010-01-28, by Christian Urban
Ported existing part of LF to new permutations and alphas.
2010-01-28, by Cezary Kaliszyk
attempt of a general abstraction operator
2010-01-28, by Christian Urban
attempt to prove equivalence between alpha definitions
2010-01-28, by Christian Urban
End of renaming.
2010-01-28, by Cezary Kaliszyk
Minor when looking at lam.distinct and lam.inject
2010-01-28, by Cezary Kaliszyk
Renamed Bexeq to Bex1_rel
2010-01-28, by Cezary Kaliszyk
Substracting bounds from free variables.
2010-01-28, by Cezary Kaliszyk
Improper interface for datatype and function packages and proper interface lateron.
2010-01-28, by Cezary Kaliszyk
merged
2010-01-28, by Christian Urban
minor
2010-01-28, by Christian Urban
test about supp/freshness for lam (old proofs work in principle - for single binders)
2010-01-28, by Christian Urban
Recommited the changes for nitpick
2010-01-28, by Cezary Kaliszyk

less more | (0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip

nominal2