The standard library for the Rocq Prover provides components for both theorem proving and efficient verified programming.
Provided functionality includes: arithmetic theorems and tactics, theorems for classical logic, algebra, real numbers, and efficient implementation of data types, for example, lists, sets, integer and floating-point numbers.
... part of T2, get it here
URL: https://rocq-prover.org/stdlib/
Author: INRIA
Maintainer: Tomas Glozar <tglozar [at] gmail [dot] com>
License: LGPL
Status: Stable
Version: 9.0.0
Download: https://github.com/rocq-prover/stdlib/tags/download/V9.0.0/ stdlib-9.0.0.tar.gz
T2 source: rocq-stdlib.cache
T2 source: rocq-stdlib.desc
Build time (on reference hardware): 230% (relative to binutils)2
Installed size (on reference hardware): 74.19 MB, 1759 files
Dependencies (build time detected): bash coreutils diffutils dune gawk grep gzip ocaml ocaml-findlib rocq sed tar zarith
Installed files (on reference hardware): n.a.
1) This page was automatically generated from the T2 package source. Corrections, such as dead links, URL changes or typos need to be performed directly on that source.
2) Compatible with Linux From Scratch's "Standard Build Unit" (SBU).