package coq-equations

You can search for identifiers within the package.

in-package search v0.2.0

A function definition package for Coq

Install

Dune Dependency

mattam82.github.io Edit opam file Versions (34)

Authors

Maintainers

M

matthieu.sozeau@inria.fr

Sources

v1.3-8.19.tar.gz

sha512=1b966b6a9fa9fbc23e46dd1238e72f326e674ce1b5c4fee1b8fb274d21cba46a5680d3bd40d0c5aa32b240f2a8c1bb14c4db4576978cd59038905e79c89e4458

Description

Equations is a function definition plugin for Coq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle.

Published: 28 Jan 2024

Dependencies (2)

ocamlfind build
coq >= "8.19" & < "8.20"

Dev Dependencies

None

Used by (13)

coq-category-theory
coq-certicoq >= "0.9+8.19"
coq-ctree
coq-hydra-battles >= "0.5"
coq-katamaran
coq-metacoq-pcuic < "1.0+8.15" | = "1.1+8.14" | = "1.1.1+8.14"
coq-metacoq-template < "1.2+8.16"
coq-metacoq-utils != "1.2.1+8.18" & != "1.3.1+8.18" & != "1.3.2+8.20" & < "1.3.4+8.20"
coq-monae >= "0.4.1" & < "0.9.2"
coq-pil
coq-ssprove < "0.3.1"
coq-verified-extraction
coq-vlsm >= "1.2"

Conflicts