package rocq-spivak
Spivak calculus, textbook exercises, real analysis, and checked tactics
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-spivak-0.1.2.tar.gz
sha256=35b85600371fbe58b9c25cb2e872725649c10b26323ae41ed798db098c19b1c2
Description
The full rocq-spivak development: all Lib, Calculus, ATTAM, and Backprop modules, including textbook exercises, Dedekind-cut reals, linear algebra, and calculus tactics. SymPy generates candidate antiderivatives; Rocq checks their derivatives and the obligations of the fundamental theorem of calculus. Completed proofs and unfinished exercises ending in Abort are included; Abort creates no theorem.
Tags
keyword:calculus keyword:tactics category:Mathematics/Real Calculus and Topology logpath:Lib logpath:Calculus logpath:ATTAM logpath:Backprop date:2026-10-03Published: 20 Oct 2026
Dependencies (12)
-
conf-boost
build -
conf-pkg-config
build -
conf-g++
build -
conf-python3-sympy
= "1" -
coq-flocq
= "4.2.2" -
coq-coquelicot
= "3.4.4" -
coq-interval
= "4.11.4" -
rocq-stdlib
= "9.1.0" -
rocq-core
= "9.1.1" -
zarith
>= "1.13" & < "2" - ocamlfind
-
ocaml
>= "4.14.1"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page