package coq-waterproof

You can search for identifiers within the package.

in-package search v0.2.0

Coq proofs in a style that resembles non-mechanized mathematical proofs

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (6)

Authors

Maintainers

J

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

Sources

2.2.0+8.20.tar.gz

md5=18c6dafc6fb018f167f89fb236ff494b

sha512=096ebe52912ebe3fb063a5ce88bee1dfc8f63226f7f1284a4304a079751b98c617a4fcafa9781c3e54e024e631c87248885b56efc20086c98ae0e525cfe08efb

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.

Published: 10 Mar 2025

Dependencies (2)

dune >= "3.6"
ocaml >= "4.09.0"

Dev Dependencies (1)

coq >= "8.20" & < "8.21" | = "dev"

Used by

None

Conflicts