]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d7b5af5) | patch
- 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
tree9598c23775d2907b1988bf7bdd39f20dcd8e3c00tree | snapshot
parentd7b5af5d8c6297f191cb644034b5b4cb7dfe86c1commit | diff
- 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 diff | blob | history
matita/matita/lib/lambda/ext_lambda.ma [new file with mode: 0644] blob
matita/matita/lib/lambda/lambda_notation.ma diff | blob | history
matita/matita/lib/lambda/subst.ma diff | blob | history
matita/matita/lib/lambda/terms.ma [new file with mode: 0644] blob
matita/matita/lib/lambda/types.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.