]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
- 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
tree9254c6e2cf2734ea367d3953042d9d3bc8db2185
parent0716716134a7820a822561cd6c55d5e71412acfd
- 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
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/notation.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
matita/matita/contribs/lambda_delta/ground_2/xoa.ma
matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma