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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Mon, 15 Mar 2021 12:10:02 +0000 (13:10 +0100)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Mon, 15 Mar 2021 12:10:02 +0000 (13:10 +0100)
commit	8fdf1af656038d0245eba64ff2531bbe94ce0e9e
tree	06ea0d9318135bbecba9fe2a75bda0ab5c724342	tree \| snapshot
parent	77c9255de3c5f7780aeacd745703a1cc76328a68	commit \| diff

propagating the arithmetics library, partial commit

+ relocation updated and ported (de Bruijn indexes now start at 1)
+ recomm updated to generate substitution files
+ results on positive integers added to arith
+ some corrections

81 files changed:

matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recommLib.ml	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/bin/recomm/recommLib.mli	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_succ.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/pnat.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/pnat_le.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/arith/pnat_le_plus.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/arith/pnat_le_pred.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/arith/pnat_lt.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/arith/pnat_lt_pred.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/pnat_pred.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/notation/relations/ratsucc_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/mr2.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/mr2_at.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/mr2_minus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream_after.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream_basic.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream_coafter.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream_eq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream_id.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream_isid.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream_istot.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/nstream_sor.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pstream.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_after.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_basic.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_coafter.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_eq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_id.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_isid.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_istot.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_sor.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_tl.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/pstream_tls.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_after.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_after_nat_uni.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_after_uni.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_at.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_at_uni.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_basic.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_basic_after.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_basic_at.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_basic_nat.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_coafter.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_coafter_uni.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_fcla.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_id.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isid.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_istot.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nat.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nat_uni.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nexts.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_pushs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_tls.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/rtmap_uni.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl		diff \| blob \| history

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

RSS Atom