nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

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

added another example which seems difficult to define
2011-07-05, by Christian Urban
added a tactic "all_trivials" which simplifies all trivial constructor cases and leaves the others untouched.
2011-07-05, by Christian Urban
merged
2011-07-05, by Christian Urban
all FCB lemmas
2011-07-05, by Christian Urban
exported various FCB-lemmas to a separate file
2011-07-05, by Christian Urban
Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?
2011-07-05, by Cezary Kaliszyk
Define a version of aux only for same binders. Completeness is fine.
2011-07-05, by Cezary Kaliszyk
Move If / Let with 'True' to the end of Lambda
2011-07-05, by Cezary Kaliszyk
merged
2011-07-04, by Christian Urban
tuned
2011-07-04, by Christian Urban
added an example that recurses over two arguments; the interesting proof-obligation is not yet done
2011-07-04, by Christian Urban
Let with a different invariant; not true.
2011-07-04, by Cezary Kaliszyk
Add non-working Lambda_F_T using FCB2
2011-07-03, by Cezary Kaliszyk
Added non-working CPS3 using FCB2
2011-07-03, by Cezary Kaliszyk
Change CPS1 to FCB2
2011-07-03, by Cezary Kaliszyk

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

nominal2