]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0716716) | patch
- relation between native type and atomic arity proced
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 15 Jun 2012 21:22:03 +0000 (21:22 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 15 Jun 2012 21:22:03 +0000 (21:22 +0000)
commit69644bb333b2862a5ff2ff434df8830e854e3385
tree9254c6e2cf2734ea367d3953042d9d3bc8db2185tree | snapshot
parent0716716134a7820a822561cd6c55d5e71412acfdcommit | diff
- relation between native type and atomic arity proced
- higher order native typing defined
- some minor results towards subject reduction for native typing
16 files changed:
matita/matita/contribs/lambda_delta/basic_2/basic_1.txt diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma [new file with mode: 0644] blob
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma [new file with mode: 0644] blob
matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma [new file with mode: 0644] blob
matita/matita/contribs/lambda_delta/basic_2/notation.ma diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma diff | blob | history
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma diff | blob | history
matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml diff | blob | history
matita/matita/contribs/lambda_delta/ground_2/xoa.ma diff | blob | history
matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.