Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-300
-100
-60
+60
+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.
First part of the description of alpha_ty.
2010-03-18, by Cezary Kaliszyk
Description of generation of alpha_bn.
2010-03-18, by Cezary Kaliszyk
case names also for _induct
2010-03-18, by Cezary Kaliszyk
Case_Names for _inducts. Does not work for _induct yet.
2010-03-18, by Cezary Kaliszyk
Added fv,bn,distinct,perm to the simplifier.
2010-03-18, by Cezary Kaliszyk
merge
2010-03-18, by Cezary Kaliszyk
Simplified the description.
2010-03-18, by Cezary Kaliszyk
merged
2010-03-18, by Christian Urban
slightly more in the paper
2010-03-18, by Christian Urban
Update the description of the generation of fv function.
2010-03-18, by Cezary Kaliszyk
fv_bn may need to call other fv_bns.
2010-03-18, by Cezary Kaliszyk
Update TODO.
2010-03-18, by Cezary Kaliszyk
Which proofs need a 'sorry'.
2010-03-18, by Cezary Kaliszyk
added TODO
2010-03-18, by Christian Urban
vixed variable names
2010-03-18, by Christian Urban
simplified strong induction proof by using flip
2010-03-18, by Christian Urban
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
Generate compound FV and Alpha for recursive bindings.
2010-03-17, by Cezary Kaliszyk
Lifting theorems with compound fv and compound alpha.
2010-03-17, by Cezary Kaliszyk
commented out examples that should not work; but for example type-scheme example should work
2010-03-17, by Christian Urban
added another supp-proof for the non-recursive case
2010-03-17, by Christian Urban
Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
2010-03-16, by Cezary Kaliszyk
merge
2010-03-16, by Cezary Kaliszyk
The old recursive alpha works fine.
2010-03-16, by Cezary Kaliszyk
added the final unfolded result
2010-03-16, by Christian Urban
merge and proof of support for non-recursive case
2010-03-16, by Christian Urban
Added Term5 non-recursive. The bug is there only for the recursive case.
2010-03-16, by Cezary Kaliszyk
Alpha is wrong.
2010-03-16, by Cezary Kaliszyk
alpha_bn doesn't need the permutation in non-recursive case.
2010-03-16, by Cezary Kaliszyk
alpha5_transp and equivp
2010-03-16, by Cezary Kaliszyk
alpha5_symp proved.
2010-03-16, by Cezary Kaliszyk
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
+1000
tip