rocq-stdlib: Stdlib for the Rocq Prover¹

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/ 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)²

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.

¹) 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.

²) Compatible with Linux From Scratch's "Standard Build Unit" (SBU).