matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 27 Aug 2011 13:59:35 +0000 (13:59 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 27 Aug 2011 13:59:35 +0000 (13:59 +0000)
commit	b264ad188cb0023a16dae105b037357fa75c5c1a
tree	42934ec11e836283a6c0e545652a17c6b643ed9c	tree \| snapshot
parent	ffe34220d80cba65eccf2396fba7f692cc6448c8	commit \| diff

- the shift function is now defined and cpr_shift_fwd is proved
- tentative definition of the structures for the wh normal forms
- definition of lists without the [...] notation
- some refactoring and annotating (we separate lemmas from facts)

31 files changed:

matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_weight.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_weight.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/grammar/leq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Basic-2/grammar/sh.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/grammar/term_simple.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Basic-2/grammar/term_weight.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Basic-2/names.txt		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/notation.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma		diff \| blob \| history
matita/matita/contribs/lambda-delta/Ground-2/arith.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Ground-2/ground.ma	[deleted file]	blob \| history
matita/matita/contribs/lambda-delta/Ground-2/list.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Ground-2/notation.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda-delta/Makefile		diff \| blob \| history

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

RSS Atom