]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fdd8107) | patch
initial version of the "lambda-delta" calculus including:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Apr 2005 11:06:01 +0000 (11:06 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Apr 2005 11:06:01 +0000 (11:06 +0000)
commitdabdf842f8f37da3d25a421740d141c28b23804a
treecb8bf658af10b6fc98ce8c26733d9c9b581ebf4atree | snapshot
parentfdd8107cc53f5e862004aa5fcd48593ee5634234commit | diff
initial version of the "lambda-delta" calculus including:

- Confluence of reduction
- Generation lemma
- Thinning lemma
- Substitution lemma
- Type Correctness
- Type Uniqueness
- Subject Reduction
helm/coq-contribs/LAMBDA-TYPES.tgz [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.