nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

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

merge
2011-06-15, by Cezary Kaliszyk
TypeSchemes work with 'default'.
2011-06-15, by Cezary Kaliszyk
tuned some proofs
2011-06-14, by Christian Urban
fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
2011-06-14, by Christian Urban
tuned
2011-06-14, by Christian Urban
Move working examples before non-working ones
2011-06-10, by Cezary Kaliszyk
Optimized proofs and removed some garbage.
2011-06-10, by Cezary Kaliszyk
merge
2011-06-10, by Cezary Kaliszyk
Slightly modify fcb for list1 and put in common place.
2011-06-10, by Cezary Kaliszyk
Experiments with Let
2011-06-10, by Cezary Kaliszyk
Eval can be defined with additional freshness
2011-06-09, by Cezary Kaliszyk
Minor simplification
2011-06-09, by Cezary Kaliszyk
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
2011-06-09, by Cezary Kaliszyk
More experiments with 'default'
2011-06-09, by Cezary Kaliszyk
Finished the proof with the invariant
2011-06-08, by Cezary Kaliszyk
Issue with 'default'
2011-06-08, by Cezary Kaliszyk
merged
2011-06-08, by Christian Urban
merged
2011-06-08, by Christian Urban
using the option "default" the function package allows one to give an explicit default value
2011-06-08, by Christian Urban
Simpler proof of TypeSchemes/substs
2011-06-08, by Cezary Kaliszyk
Simplify fcb_res
2011-06-08, by Cezary Kaliszyk
FCB for res binding and simplified proof of subst for type schemes
2011-06-08, by Cezary Kaliszyk
Simplify ln-trans proof
2011-06-08, by Cezary Kaliszyk
cbvs can be easily defined without an invariant
2011-06-08, by Cezary Kaliszyk
defined the "count-bound-variables-occurences" function which has an accumulator like trans
2011-06-07, by Christian Urban
merged
2011-06-07, by Christian Urban
remove garbage (proofs that assumes the invariant outside function)
2011-06-07, by Cezary Kaliszyk
Proof of trans with invariant
2011-06-07, by Cezary Kaliszyk
Testing invariant in Lambda_F_T
2011-06-07, by Cezary Kaliszyk
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
2011-06-07, by Christian Urban
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
2011-06-07, by Christian Urban
slightly stronger property in fundef_ex_prop
2011-06-06, by Christian Urban
added an option for an invariant (at the moment only a stub)
2011-06-05, by Christian Urban
added a more general lemma fro fundef_ex1
2011-06-05, by Christian Urban
Trying the induction on the graph
2011-06-04, by Cezary Kaliszyk
Finish and test the locale approach
2011-06-04, by Cezary Kaliszyk
FiniteSupp precondition in the function is enough to get rid of completeness obligationss
2011-06-03, by Cezary Kaliszyk
recursion combinator inside a locale
2011-06-03, by Christian Urban
merge
2011-06-03, by Cezary Kaliszyk
F for lambda used to define translation to locally nameless
2011-06-03, by Cezary Kaliszyk
typo
2011-06-02, by Christian Urban
removed dead code
2011-06-02, by Christian Urban
finished the missing obligations
2011-06-02, by Cezary Kaliszyk
merged
2011-06-02, by Christian Urban
a test with a recursion combinator defined on top of nominal_primrec
2011-06-02, by Christian Urban
Use FCB to simplify proof
2011-06-02, by Cezary Kaliszyk
merge
2011-06-02, by Cezary Kaliszyk
Remove SMT
2011-06-02, by Cezary Kaliszyk
hopefully final fix for ho-functions
2011-06-01, by Christian Urban
first test to fix the problem with free variables
2011-06-01, by Christian Urban
proved subst for All constructor in type schemes.
2011-06-01, by Cezary Kaliszyk
DB translation using index; easier to reason about.
2011-06-01, by Cezary Kaliszyk
Problem: free variables in the goal
2011-06-01, by Cezary Kaliszyk
fixed previous commit
2011-06-01, by Cezary Kaliszyk
equivariance of db_trans
2011-06-01, by Cezary Kaliszyk
fixed the problem with cps-like functions
2011-05-31, by Christian Urban
DeBruijn translation in a simplifier friendly way
2011-05-31, by Cezary Kaliszyk
map_term can be defined when equivariance is assumed
2011-05-31, by Cezary Kaliszyk
map_term is not a function the way it is defined
2011-05-31, by Cezary Kaliszyk
Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
2011-05-31, by Cezary Kaliszyk

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

nominal2