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

Authors

Maintainers

M

matthieu.sozeau@inria.fr

Sources

v1.3-8.18.tar.gz

sha512=07d02b5a5927c4dd36716d68c600e7c02955b08bd63b8e74f2b7e39e939cdd92a46b3c51cb2db3a882d193dc3ec94c81254cac18efe5909edfd8ea5aec444666

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: 13 Sep 2023

Dependencies (2)

ocamlfind build
coq >= "8.18~" & < "8.19"

Dev Dependencies

None

Used by (11)

coq-category-theory
coq-hydra-battles >= "0.5"
coq-katamaran
coq-metacoq-checker = "1.0~alpha2+8.10" | = "1.0~beta1+8.11"
coq-metacoq-pcuic != "1.0~beta1+8.12" & < "1.0~beta2+8.12" | = "1.0+8.14" | = "1.1+8.14" | = "1.1.1+8.14"
coq-metacoq-template >= "1.0~alpha2+8.10" & < "1.0~beta1+8.11" | >= "1.0~beta2+8.11" & < "1.2+8.16"
coq-metacoq-utils < "1.3.1+8.19"
coq-monae >= "0.4.1"
coq-pil
coq-ssprove
coq-vlsm >= "1.2"

Conflicts