]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 08726a4) | patch
- nat: some additions, plus_minus_commutative renamed plus_minus_associative
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 26 Jan 2014 10:08:33 +0000 (10:08 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 26 Jan 2014 10:08:33 +0000 (10:08 +0000)
commitcdf346ea9e5dd3842c67e0f0595e110a07c0094c
treec89e99966bd4450d4157623b18c44ec88fcc634btree | snapshot
parent08726a4392355fb8340894b1dcabccf95d46b565commit | diff
- nat: some additions, plus_minus_commutative renamed plus_minus_associative
- lambda: we study terms in which references are by "level" rather
than by "depth" aiming at establishing a bijection between the two
representations, we start the support for distributed notation as in lambdadelta
matita/matita/lib/arithmetics/chebyshev/bertrand.ma diff | blob | history
matita/matita/lib/arithmetics/chebyshev/psi_bounds.ma diff | blob | history
matita/matita/lib/arithmetics/nat.ma diff | blob | history
matita/matita/lib/lambda/background/notation.ma diff | blob | history
matita/matita/lib/lambda/levels/interpretations.ma [new file with mode: 0644] blob
matita/matita/lib/lambda/levels/term.ma [new file with mode: 0644] blob
matita/matita/lib/lambda/notation/functions/backward_1.ma [new file with mode: 0644] blob
matita/matita/lib/lambda/notation/functions/backward_3.ma [new file with mode: 0644] blob
matita/matita/lib/lambda/notation/functions/forward_1.ma [new file with mode: 0644] blob
matita/matita/lib/lambda/notation/functions/forward_3.ma [new file with mode: 0644] blob
matita/matita/lib/lambda/terms/iterated_abstraction.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.