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

sha256=48fcb716c00d52802a9596ee396eab9af7f368da6afebdbb9cf67738ae133b97

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.7.2" & < "8.8~"

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