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.2.1-8.10-2.tar.gz

sha512=f95dc46d905a28e62846991fa9612476019f933ac7bee2117f1d1c17a2ea78c66f925d14dd11534c29526fe9cabc77efd7fea78b0a32c82af0c50360b4a123fb

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: 05 Nov 2019

Dependencies (1)

coq >= "8.10~" & < "8.11~"

Dev Dependencies

None

Used by (8)

coq-category-theory
coq-hydra-battles
coq-katamaran < "0.2.0"
coq-metacoq-checker >= "1.0~alpha2+8.10" & < "1.0~beta1+8.11"
coq-metacoq-pcuic < "1.0~beta1+8.11"
coq-metacoq-template >= "1.0~alpha2+8.10" & < "1.0~beta1+8.11"
coq-pil
coq-vlsm >= "1.2"

Conflicts