package coq-equations

  1. Overview
  2. Homepage
A function definition package for Coq

Install

Dune Dependency

Authors

Maintainers

Sources

v1.3-8.19.tar.gz
sha512=932facad3e04a3629185a43171dd16efedde649f8f1ecc858eed6b863eae6abff7ecfb4fd1345e31ec9c53f88cba3482da2ccb4e7f6aabf004cc95e2318abe56

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.

Dependencies (2)

  1. ocamlfind build
  2. coq >= "8.19" & < "8.20"

Dev Dependencies

None

Used by (13)

  1. coq-category-theory
  2. coq-certicoq >= "0.9+8.19"
  3. coq-hydra-battles >= "0.5"
  4. coq-katamaran
  5. coq-metacoq-checker = "1.0~alpha2+8.10" | = "1.0~beta1+8.11"
  6. 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"
  7. coq-metacoq-template >= "1.0~alpha2+8.10" & < "1.0~beta1+8.11" | >= "1.0~beta2+8.11" & < "1.2+8.16"
  8. coq-metacoq-utils != "1.2.1+8.18" & != "1.3.1+8.18" & != "1.3.2+8.20" & < "1.3.4+8.20"
  9. coq-monae >= "0.4.1"
  10. coq-pil
  11. coq-ssprove
  12. coq-verified-extraction
  13. coq-vlsm >= "1.2"

Conflicts

None

Rocq

Interactive Theorem Prover