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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 26 Feb 2021 13:21:42 +0000 (14:21 +0100)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 26 Feb 2021 13:21:42 +0000 (14:21 +0100)
commit	dbc57c92512c04b3fd88f8289bb8dbe99b2f90e0
tree	16af112269d5b6dfe051c3e218a2a2f64132d989	tree \| snapshot
parent	baa54e5db0fb93c4242dd1b67a5018ca63206cf6	commit \| diff

propagating the arithmetics library, partial commit

+ counters (was: steps) ported and restyled
+ core notation: "pair" decentralized
+ some corrections and renaming

60 files changed:

.gitignore		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/Makefile		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc	[new file with mode: 0644]	blob
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/recommGc.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.mli	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll		diff \| blob \| history
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/recommPccFor.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/counters/rtc.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_max.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_max_shift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_shift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_max.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_shift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_max_shift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_plus.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/counters/rtc_shift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/notation/relations/isredtype_2.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/notation/relations/istotal_1.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/notation/relations/istype_2.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_max.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_max_shift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_plus.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_shift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_ist.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_max.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_plus.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_shift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_max.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_max_shift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_plus.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_shift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl		diff \| blob \| history
matita/matita/lib/basics/core_notation.ma		diff \| blob \| history
matita/matita/lib/basics/core_notation/pair_2.ma	[new file with mode: 0644]	blob
matita/matita/lib/basics/types.ma		diff \| blob \| history
matita/matita/lib/hott/notations.ma		diff \| blob \| history

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

RSS Atom