Bug#1111824: ITP: rocq-stdlib -- Rocq's Standard library
Package: wnpp
Severity: wishlist
Owner: Julien Puydt <jpuydt@debian.org>
X-Debbugs-Cc: debian-devel@lists.debian.org, Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>, jpuydt@debian.org
* Package name : rocq-stdlib
Version : 9.0.0
Upstream Contact: Rocq Development Team
* URL : https://rocq-prover.org
* License : LGPL-2.1
Programming Lang: Rocq, OCaml
Description : Rocq's Standard library
Rocq is a proof asssistant for higher-order logic, which
allows the development of computer programs consistent with
their formal specification. It is developed using Objective
Caml and Camlp5.
.
This package provides the Rocq Standard Library, about
basic numbers, sets, lists, strings and other basic concepts.
The Coq proof assistant is becoming the Rocq theorem prover ('coq' didn't sound
professional on an international level...) ; and with this change upstream is
also splitting its standard library into a core (which stays with the main
package) and a standard library (which is this new package is about). I plan to
maintain this package along with the rest of the Coq/Rocq ecosystem within the
OCaml Maintainers team.
Cheers,
J.Puydt
Reply to: