]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c1f4f61) | patch
Added a demo for Matita: two slightly different proofs in declarative language
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2006 21:48:29 +0000 (21:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2006 21:48:29 +0000 (21:48 +0000)
commit16bd8ab4cb83990229256fb9aa65c94f90f25c5d
tree0669f2676b8be1cbb8d10f9347600462fc41fe2btree | snapshot
parentc1f4f612cb879d0295f8ac1491a12acc783194d9commit | diff
Added a demo for Matita: two slightly different proofs in declarative language
that the derivative of x^n is n*x^(n-1). The real numbers, the definition of
derivative and some basic properties of derivatives are axiomatized. Two
alternative notations are proposed for the derivatives. (The somehow nicer
one is currently bugged.)
matita/library/demo/power_derivative.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.