package coq-waterproof

  1. Overview
  2. No Docs
Coq proofs in a style that resembles non-mechanized mathematical proofs

Install 

dune-project
 Dependency

github.com Edit opam file Versions (12)

Authors

  1. J
    Jelle 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.0+9.0.tar.gz
md5=7cfe30aceb61e154ed905e048bdf2cb7
sha512=006bf05727d2aa21cebe332ff5a027fdd8843c574753fd5b8d0486e4df7bd447a4f538c3c92736011734c29c601d3a77c2f1a1ee5b3645a7666766ed32907777

Description

The Waterproof plugin for the Coq proof assistant allows you to write Coq 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

Published: 04 Nov 2025

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"

Used by

None