2010-02-10 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
Fixed rbv6, when translating to OTT.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
Some cleaning of proofs.
|
changeset |
files
|
2010-02-10 |
Christian Urban |
merged again
|
changeset |
files
|
2010-02-10 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
more minor space and bracket modifications.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
More changes according to the standards.
|
changeset |
files
|
2010-02-10 |
Cezary Kaliszyk |
A concrete example, with a proof that rbv is not regular and
|
changeset |
files
|
2010-02-09 |
Christian Urban |
proper declaration of types and terms during parsing (removes the varifyT when storing data)
|
changeset |
files
|
2010-02-09 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-09 |
Christian Urban |
slight correction
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
More about trm6
|
changeset |
files
|
2010-02-09 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
the specifications of the respects.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
trm6 with the 'Foo' constructor.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
removing unnecessary brackets
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
More indentation cleaning.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
'exc' -> 'exn' and more name and space cleaning.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Fully qualified exception names.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
More indentation, names and todo cleaning in the quotient package
|
changeset |
files
|
2010-02-09 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-09 |
Christian Urban |
a few more attempts to show the equivalence between old and new way of defining alpha-equivalence
|
changeset |
files
|
2010-02-09 |
Christian Urban |
minor tuning
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Explicitly marked what is bound.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Cleaning and updating in Terms.
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Looking at the trm2 example
|
changeset |
files
|
2010-02-09 |
Cezary Kaliszyk |
Fixed pattern matching, now the test in Abs works correctly.
|
changeset |
files
|
2010-02-08 |
Christian Urban |
added a test case
|
changeset |
files
|
2010-02-08 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-08 |
Christian Urban |
moved some lemmas to Nominal; updated all files
|
changeset |
files
|
2010-02-08 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-08 |
Cezary Kaliszyk |
Comments.
|
changeset |
files
|
2010-02-08 |
Christian Urban |
slightly tuned
|
changeset |
files
|
2010-02-08 |
Cezary Kaliszyk |
Proper context fixes lifting inside instantiations.
|
changeset |
files
|
2010-02-08 |
Cezary Kaliszyk |
Fixed the context import/export and simplified LFex.
|
changeset |
files
|
2010-02-08 |
Christian Urban |
added 2 papers about core haskell
|
changeset |
files
|
2010-02-07 |
Christian Urban |
fixed lemma name
|
changeset |
files
|
2010-02-07 |
Christian Urban |
updated to latest Nominal2
|
changeset |
files
|
2010-02-06 |
Christian Urban |
minor
|
changeset |
files
|
2010-02-06 |
Christian Urban |
some tuning
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
Fixes for Bex1 removal.
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
A procedure that properly instantiates the types too.
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
More code abstracted away
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
A bit more intelligent and cleaner code.
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-05 |
Cezary Kaliszyk |
A proper version of the attribute
|
changeset |
files
|
2010-02-05 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-05 |
Christian Urban |
eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts
|
changeset |
files
|
2010-02-04 |
Cezary Kaliszyk |
The automatic lifting translation function, still with dummy types,
|
changeset |
files
|
2010-02-04 |
Cezary Kaliszyk |
Quotdata_dest needed for lifting theorem translation.
|
changeset |
files
|
2010-02-04 |
Christian Urban |
fixed (permute_eqvt in eqvts makes this simpset always looping)
|
changeset |
files
|
2010-02-04 |
Christian Urban |
rollback of the test
|
changeset |
files
|
2010-02-04 |
Christian Urban |
linked versions - instead of copies
|
changeset |
files
|
2010-02-04 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-04 |
Christian Urban |
restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
More let-rec experiments
|
changeset |
files
|
2010-02-03 |
Christian Urban |
proposal for an alpha equivalence
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Lets different.
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Simplified the proof.
|
changeset |
files
|
2010-02-03 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-03 |
Christian Urban |
proved that bv for lists respects alpha for terms
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Finished remains on the let proof.
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Lets are ok.
|
changeset |
files
|
2010-02-03 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-03 |
Christian Urban |
added type-scheme example
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Definitions for trm5
|
changeset |
files
|
2010-02-03 |
Christian Urban |
another adaptation for the eqvt-change
|
changeset |
files
|
2010-02-03 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-03 |
Christian Urban |
fixed proofs that broke because of eqvt
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Minor fix.
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
alpha5 pseudo-injective
|
changeset |
files
|
2010-02-03 |
Christian Urban |
fixed proofs in Abs.thy
|
changeset |
files
|
2010-02-03 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-03 |
Christian Urban |
added a first eqvt_tac which pushes permutations inside terms
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
The alpha-equivalence relation for let-rec. Not sure if correct...
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Starting with a let-rec example.
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Minor
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
Some cleaning and eqvt proof
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
The trm1_support lemma explicitly and stated a strong induction principle.
|
changeset |
files
|
2010-02-03 |
Cezary Kaliszyk |
More ingredients in Terms.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
More in Terms
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
First experiments in Terms.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
Disambiguating the syntax.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
Minor uncommited changes from LamEx2.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
Some equivariance machinery that comes useful in LF.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
Generalized the eqvt proof for single binders.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
With induct instead of induct_tac, just one induction is sufficient.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
General alpha_gen_trans for one-variable abstraction.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
With unfolding Rep/Abs_eqvt no longer needed.
|
changeset |
files
|
2010-02-02 |
Cezary Kaliszyk |
Lam2 finished apart from Rep_eqvt.
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
All should be ok now.
|
changeset |
files
|
2010-02-01 |
Christian Urban |
repaired according to changes in Abs.thy
|
changeset |
files
|
2010-02-01 |
Christian Urban |
added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case
|
changeset |
files
|
2010-02-01 |
Christian Urban |
cleaned
|
changeset |
files
|
2010-02-01 |
Christian Urban |
updated from huffman
|
changeset |
files
|
2010-02-01 |
Christian Urban |
updated from nominal-huffman
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
Fixed wrong rename.
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
Lambda based on alpha_gen, under construction.
|
changeset |
files
|
2010-02-01 |
Christian Urban |
updated from huffman - repo
|
changeset |
files
|
2010-02-01 |
Christian Urban |
renamed Abst/abst to Abs/abs
|
changeset |
files
|
2010-02-01 |
Christian Urban |
got rid of RAbst type - is now just pairs
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
Monotonicity of ~~gen, needed for using it in inductive definitions.
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
The current state of fv vs supp proofs in LF.
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
2010-02-01 |
Cezary Kaliszyk |
More proofs in the LF example.
|
changeset |
files
|
2010-02-01 |
Christian Urban |
merged
|
changeset |
files
|
2010-02-01 |
Christian Urban |
slight tuning
|
changeset |
files
|
2010-02-01 |
Christian Urban |
renamed function according to the name of the constant
|
changeset |
files
|