| Sat, 30 Jan 2010 12:12:52 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Sat, 30 Jan 2010 11:44:25 +0100 |
Christian Urban |
introduced a generic alpha (but not sure whether it is helpful)
|
changeset |
files
|
| Fri, 29 Jan 2010 19:42:07 +0100 |
Cezary Kaliszyk |
More in the LF example in the new nominal way, all is clear until support.
|
changeset |
files
|
| Fri, 29 Jan 2010 13:47:05 +0100 |
Cezary Kaliszyk |
Fixed the induction problem + some more proofs.
|
changeset |
files
|
| Fri, 29 Jan 2010 12:16:08 +0100 |
Cezary Kaliszyk |
equivariance of rfv and alpha.
|
changeset |
files
|
| Fri, 29 Jan 2010 10:13:07 +0100 |
Cezary Kaliszyk |
Added the experiments with fun and function.
|
changeset |
files
|
| Fri, 29 Jan 2010 07:09:52 +0100 |
Christian Urban |
now also final step is proved - the supp of lambdas is now completely characterised
|
changeset |
files
|
| Fri, 29 Jan 2010 00:22:00 +0100 |
Christian Urban |
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms
|
changeset |
files
|
| Thu, 28 Jan 2010 23:47:02 +0100 |
Christian Urban |
improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
|
changeset |
files
|
| Thu, 28 Jan 2010 23:36:58 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Thu, 28 Jan 2010 23:36:38 +0100 |
Christian Urban |
general abstraction operator and complete characterisation of its support and freshness
|
changeset |
files
|
| Thu, 28 Jan 2010 19:23:55 +0100 |
Cezary Kaliszyk |
Ported existing part of LF to new permutations and alphas.
|
changeset |
files
|
| Thu, 28 Jan 2010 15:47:35 +0100 |
Christian Urban |
attempt of a general abstraction operator
|
changeset |
files
|
| Thu, 28 Jan 2010 14:20:26 +0100 |
Christian Urban |
attempt to prove equivalence between alpha definitions
|
changeset |
files
|
| Thu, 28 Jan 2010 12:28:50 +0100 |
Cezary Kaliszyk |
End of renaming.
|
changeset |
files
|
| Thu, 28 Jan 2010 12:25:38 +0100 |
Cezary Kaliszyk |
Minor when looking at lam.distinct and lam.inject
|
changeset |
files
|
| Thu, 28 Jan 2010 12:24:49 +0100 |
Cezary Kaliszyk |
Renamed Bexeq to Bex1_rel
|
changeset |
files
|
| Thu, 28 Jan 2010 10:52:10 +0100 |
Cezary Kaliszyk |
Substracting bounds from free variables.
|
changeset |
files
|
| Thu, 28 Jan 2010 10:26:36 +0100 |
Cezary Kaliszyk |
Improper interface for datatype and function packages and proper interface lateron.
|
changeset |
files
|
| Thu, 28 Jan 2010 09:28:20 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Thu, 28 Jan 2010 09:28:06 +0100 |
Christian Urban |
minor
|
changeset |
files
|
| Thu, 28 Jan 2010 01:24:09 +0100 |
Christian Urban |
test about supp/freshness for lam (old proofs work in principle - for single binders)
|
changeset |
files
|
| Thu, 28 Jan 2010 08:13:39 +0100 |
Cezary Kaliszyk |
Recommited the changes for nitpick
|
changeset |
files
|
| Wed, 27 Jan 2010 18:26:01 +0100 |
Cezary Kaliszyk |
Correct types which fixes the printing.
|
changeset |
files
|
| Wed, 27 Jan 2010 18:06:14 +0100 |
Cezary Kaliszyk |
fv for subterms
|
changeset |
files
|
| Wed, 27 Jan 2010 17:39:13 +0100 |
Cezary Kaliszyk |
Fix the problem with later examples. Maybe need to go back to textual specifications.
|
changeset |
files
|
| Wed, 27 Jan 2010 17:18:30 +0100 |
Cezary Kaliszyk |
Some processing of variables in constructors to get free variables.
|
changeset |
files
|
| Wed, 27 Jan 2010 16:40:16 +0100 |
Cezary Kaliszyk |
Parsing of the input as terms and types, and passing them as such to the function package.
|
changeset |
files
|
| Wed, 27 Jan 2010 16:07:49 +0100 |
Cezary Kaliszyk |
Undid the parsing, as it is not possible with thy->lthy interaction.
|
changeset |
files
|
| Wed, 27 Jan 2010 14:57:11 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|