matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda_delta/basic

]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Wed, 30 May 2012 21:10:44 +0000 (21:10 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Wed, 30 May 2012 21:10:44 +0000 (21:10 +0000)
commit	5ac2dc4e01aca542ddd13c02b304c646d8df9799
tree	f4baf23e1321a2b646c77d5201d85f4e47344759	tree \| snapshot
parent	a386e0eb6b20909ae78c825203d77647b8fde30c	commit \| diff

- nDestructTac: Sys.break handled in two places
- lambda_delta: a major property of native type assignment
some properties of context sensitive equivalence
some notational changes
some annotations

38 files changed:

matita/components/ng_tactics/nDestructTac.ml		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/basic_1.txt		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.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/equivalence/cpcs_ltpr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/notation.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.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/reducibility/lcpr_cpr.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma		diff \| blob \| history
matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom