package coq-paramcoq

You can search for identifiers within the package.

in-package search v0.2.0

Plugin for generating parametricity statements to perform refinement proofs

Install

Dune Dependency

github.com Edit opam file Versions (26)

Authors

Maintainers

P

Pierre Roux <pierre.roux@onera.fr>

Sources

v1.1.2+coq8.8.tar.gz

sha256=fc5815f7ff04adf188ba7dbdd2e70ec46395e3c544fd1355a79d10ceb447b7d0

Description

The plugin is still in an experimental state. It is not very user friendly (lack of good error messages) and still contains bugs. But is useable enough to "translate" a large chunk of standard library.

Published: 13 Nov 2019

Dependencies (1)

coq >= "8.8" & < "8.9~"

Dev Dependencies

None

Used by (4)

coq-addition-chains < "0.5"
coq-coqeal < "1.1.0"
coq-monae >= "0.1.1" & < "0.4"
coq-validsdp < "1.0.4"

Conflicts