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

sha256=beec196a00bc7a25b892349070d6371511f817623cdeb379f7cf827d0f823c4f

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: 10 Aug 2020

Dependencies (3)

ocamlfind build
ocaml
coq >= "8.12" & < "8.13~"

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