]> matita.cs.unibo.it Git - helm.git/commit
- lambda_notation.ma: more notation and bug fixes
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 22 Mar 2011 18:53:26 +0000 (18:53 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 22 Mar 2011 18:53:26 +0000 (18:53 +0000)
commitffbc6cd1358d61072105766052c7498a1f37c769
tree9598c23775d2907b1988bf7bdd39f20dcd8e3c00
parentd7b5af5d8c6297f191cb644034b5b4cb7dfe86c1
- lambda_notation.ma: more notation and bug fixes
- terms.ma: contains the data structure of terms and related functions (not involving substitution).
- ext_lambda.ma: cut off of previous ext.ma, containing the lambda-related objects
- subst.ma, types.ma: we removed notation from here
- types.ma: we added special cases of the weakening and thinning lemmas as axioms
matita/matita/lib/lambda/ext.ma
matita/matita/lib/lambda/ext_lambda.ma [new file with mode: 0644]
matita/matita/lib/lambda/lambda_notation.ma
matita/matita/lib/lambda/subst.ma
matita/matita/lib/lambda/terms.ma [new file with mode: 0644]
matita/matita/lib/lambda/types.ma