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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
cleaned
2010-02-01, by Christian Urban
updated from huffman
2010-02-01, by Christian Urban
updated from nominal-huffman
2010-02-01, by Christian Urban
Fixed wrong rename.
2010-02-01, by Cezary Kaliszyk
merge
2010-02-01, by Cezary Kaliszyk
Lambda based on alpha_gen, under construction.
2010-02-01, by Cezary Kaliszyk
updated from huffman - repo
2010-02-01, by Christian Urban
renamed Abst/abst to Abs/abs
2010-02-01, by Christian Urban
got rid of RAbst type - is now just pairs
2010-02-01, by Christian Urban
Monotonicity of ~~gen, needed for using it in inductive definitions.
2010-02-01, by Cezary Kaliszyk
The current state of fv vs supp proofs in LF.
2010-02-01, by Cezary Kaliszyk
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
less
more
|
(0)
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
tip