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.
Rename bound variables + minor cleaning.
2010-03-18, by Cezary Kaliszyk
Move most of the exporting out of the parser.
2010-03-18, by Cezary Kaliszyk
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
2010-03-18, by Cezary Kaliszyk
Prove eqvts on exported terms.
2010-03-18, by Cezary Kaliszyk
Clean 'Lift', start working only on exported things in Parser.
2010-03-18, by Cezary Kaliszyk
slightly more of the paper
2010-03-18, by Christian Urban
merged
2010-03-17, by Christian Urban
paper uses now a heap file - does not compile so long anymore
2010-03-17, by Christian Urban
merge
2010-03-17, by Cezary Kaliszyk
compose_sym2 works also for term5
2010-03-17, by Cezary Kaliszyk
Updated Term1, including statement of strong induction.
2010-03-17, by Cezary Kaliszyk
Proper compose_sym2
2010-03-17, by Cezary Kaliszyk
merged
2010-03-17, by Christian Urban
temporarily disabled tests in Nominal/ROOT
2010-03-17, by Christian Urban
made paper to compile
2010-03-17, by Christian Urban
added partial proof for the strong induction principle
2010-03-17, by Christian Urban
Trying to find a compose lemma for 2 arguments.
2010-03-17, by Cezary Kaliszyk
merge
2010-03-17, by Cezary Kaliszyk
cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
2010-03-17, by Cezary Kaliszyk
merged
2010-03-17, by Christian Urban
added proof of supp/fv for type schemes
2010-03-17, by Christian Urban
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
2010-03-17, by Cezary Kaliszyk
Remove Term5a, since it is now identical to Term5.
2010-03-17, by Cezary Kaliszyk
merge
2010-03-17, by Cezary Kaliszyk
Finished all proofs in Term5 and Term5n.
2010-03-17, by Cezary Kaliszyk
added partial proof of supp for type schemes
2010-03-17, by Christian Urban
Fix in alpha; support of the recursive Let works :)
2010-03-17, by Cezary Kaliszyk
The recursive supp just has one equation too much.
2010-03-17, by Cezary Kaliszyk
Fix for the change of alpha_gen.
2010-03-17, by Cezary Kaliszyk
merge
2010-03-17, by Cezary Kaliszyk
less
more
|
(0)
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
tip