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 +1000 tip

Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02, by Cezary Kaliszyk
merged
2010-03-02, by Christian Urban
rawified the bind specs (ready to be used now)
2010-03-02, by Christian Urban
merge
2010-03-01, by Cezary Kaliszyk
Trying to prove equivariance.
2010-03-01, by Cezary Kaliszyk
modified for new binding format - hope it is the intended one
2010-03-01, by Christian Urban
further code-refactoring in the parser
2010-03-01, by Christian Urban
The new alpha-equivalence and testing in Trm2 and Trm5.
2010-03-01, by Cezary Kaliszyk
slight simplification of the raw-decl generation
2010-03-01, by Christian Urban
Example that shows that current alpha is wrong.
2010-03-01, by Cezary Kaliszyk
added example from my phd
2010-03-01, by Christian Urban
streamlined parser
2010-02-27, by Christian Urban
generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
2010-02-26, by Christian Urban
More about the general lifting procedure.
2010-02-26, by Cezary Kaliszyk
Update TODO
2010-02-26, by Cezary Kaliszyk
Progress with general lifting procedure.
2010-02-26, by Cezary Kaliszyk
RSP of perms can be shown in one go.
2010-02-26, by Cezary Kaliszyk
Change in signature of prove_const_rsp for general lifting.
2010-02-26, by Cezary Kaliszyk
Permutation and FV_Alpha interface change.
2010-02-26, by Cezary Kaliszyk
To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-26, by Cezary Kaliszyk
merge
2010-02-25, by Cezary Kaliszyk
Preparing the generalized lifting procedure
2010-02-25, by Cezary Kaliszyk
merged
2010-02-25, by Christian Urban
added ott-example about Leroy96
2010-02-25, by Christian Urban
Forgot to add one file.
2010-02-25, by Cezary Kaliszyk
Split Terms into separate files and add them to tests.
2010-02-25, by Cezary Kaliszyk
merge
2010-02-25, by Cezary Kaliszyk
Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25, by Cezary Kaliszyk
merged
2010-02-25, by Christian Urban
a few simplifications
2010-02-25, by Christian Urban
first attempt to make sense out of the core-haskell definition
2010-02-25, by Christian Urban
Code for proving eqvt, still in Terms.
2010-02-25, by Cezary Kaliszyk
Use eqvt infrastructure.
2010-02-25, by Cezary Kaliszyk
Simple function eqvt code.
2010-02-25, by Cezary Kaliszyk
added IsaMakefile...but so far included only a test for the parser
2010-02-25, by Christian Urban
moved Quot package to Attic (still compiles there with "isabelle make")
2010-02-25, by Christian Urban
merged
2010-02-25, by Christian Urban
moved Nominal to "toplevel"
2010-02-25, by Christian Urban
Export perm_frees.
2010-02-25, by Cezary Kaliszyk
Restructuring the code in Perm
2010-02-24, by Cezary Kaliszyk
Simplified and finised eqvt proofs for t1 and t5
2010-02-24, by Cezary Kaliszyk
merge
2010-02-24, by Cezary Kaliszyk
Define lifted perms.
2010-02-24, by Cezary Kaliszyk
merged
2010-02-24, by Christian Urban
parsing and definition of raw datatype and bv-function work (not very beautiful)
2010-02-24, by Christian Urban
With permute_rsp we can lift the instance proofs :).
2010-02-24, by Cezary Kaliszyk
Note the instance proofs, since they can be easily lifted.
2010-02-24, by Cezary Kaliszyk
More refactoring and removed references to the global simpset in Perm.
2010-02-24, by Cezary Kaliszyk
Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
2010-02-24, by Cezary Kaliszyk
Regularize finite support proof for trm1
2010-02-24, by Cezary Kaliszyk
Made the fv-supp proof much more straightforward.
2010-02-24, by Cezary Kaliszyk
Regularize the proofs about finite support.
2010-02-24, by Cezary Kaliszyk
Respects of permute and constructors.
2010-02-24, by Cezary Kaliszyk
Generate fv_rsp automatically.
2010-02-24, by Cezary Kaliszyk
Define the constants automatically.
2010-02-24, by Cezary Kaliszyk
Rename also the lifted types to non-capital.
2010-02-24, by Cezary Kaliszyk
Use the infrastructure in LF. Much shorter :).
2010-02-24, by Cezary Kaliszyk
Final synchronization of names.
2010-02-24, by Cezary Kaliszyk
LF renaming part 3 (proper names of alpha equvalences)
2010-02-24, by Cezary Kaliszyk
LF renaming part 2 (proper fv functions)
2010-02-24, by Cezary Kaliszyk

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

nominal2