]> matita.cs.unibo.it Git - helm.git/commit
arithmetics for λδ
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 28 Dec 2020 18:43:58 +0000 (19:43 +0100)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 28 Dec 2020 18:43:58 +0000 (19:43 +0100)
commit5e72e41f4f86814e56d4b00959ccc56c71042a4c
treea78b706fdf5aa6f9281a959925befdbfead1c1e6
parent74c6905907b0bca229366d52450e2a6982b5b8be
arithmetics for λδ

+ subtraction for non-negative integers
+ web site update
+ apps_2/examples: minor update
25 files changed:
helm/www/lambdadelta/images/bronze-03B4.png
helm/www/lambdadelta/images/bronze-03BB.png
matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma
matita/matita/contribs/lambdadelta/ground/arith/nat.txt
matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma
matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl