]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambdadelta/ground/wf_ind/wf3_ind_nlt.ma
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 614d006) | patch
arithmetics for λδ
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Sat, 19 Dec 2020 19:18:17 +0000 (20:18 +0100)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Sat, 19 Dec 2020 19:18:17 +0000 (20:18 +0100)
commitdf7a2aa19e98dc28e7f22129275a175cead49e2d
treecdb036f4e78a6d36549aa1c583e63bc8518fdf9atree | snapshot
parent614d006be363d2e2bbfdf8eb3c20c8604d278be1commit | diff
arithmetics for λδ

we rebild the arithmetic library because lib/arithmetics/nat.ma has some problems:
- matitac does not compile it because of known time travel erropr
- too many indexed theorems make the search space explode during auto
18 files changed:
matita/matita/contribs/lambdadelta/ground/arith/nat.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/nat.txt [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/nat_iter_succ.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/pnat.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/wf_ind/wf1_ind_nlt.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/wf_ind/wf2_ind_nlt.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/ground/wf_ind/wf3_ind_nlt.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.