package rocq-waterproof

Build not yet checked
  1. Overview
  2. No Docs
Rocq proofs in a style that resembles non-mechanized mathematical proofs

Install 

dune-project
 Dependency

github.com Edit opam file Versions (1)

Authors

  1. J
    Jente Wemmenhove
  2. P
    Pim Otte
  3. B
    Balthazar Pathiachvili
  4. D
    Dick Arends
  5. C
    Cosmin Manea
  6. L
    Lulof Pirée
  7. A
    Adrian Vrămuleţ
  8. T
    Tudor Voicu
  9. J
    Jim Portegies <j.w.portegies@tue.nl>

Maintainers

  1. J
    Jim Portegies <j.w.portegies@tue.nl>

Sources

3.1.1+9.0.tar.gz
md5=0868778101a2429e98ffdf3e6b761ffd
sha512=c77e50b841b9c24368bda3534e36687ade5eb8e683b493ff83bd4a4a5652851d42b759a0461cd6c512af6fdcf767f3a0b612d4c00054b860c6cba46f5537f6cd

Description

The Waterproof plugin for the Rocq proof assistant allows you to write Rocq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.

Tags

keyword:mathematics education category:Mathematics/Education date:2023-11-04 logpath:Waterproof

Added to opam-repository:

Dependencies (2)

  1. dune >= "3.8"
  2. ocaml >= "4.09.0"

Dev Dependencies (2)

  1. coq >= "9.0" & < "9.1" | = "dev"
  2. rocq-prover >= "9.0" & < "9.1" | = "dev"

Optional Dependencies

None

Used by

None

Conflicts

None

Build status

This version of rocq-waterproof was published after the check.ci.ocaml.org run of against opam-repository 8a77e58, so it has no build results yet. check.ci runs about once a week.