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.10.tar.gz

sha256=e48c38685ee0efee81002ef916a3856832c9f6712b9e12394a7824f944a8631c

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 (3)

ocamlfind build
ocaml
coq >= "8.10" & < "8.11~"

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