package coq-equations

  1. Overview
  2. No Docs
A function definition package for Coq

Install

Dune Dependency

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

Authors

  1. M
    Matthieu Sozeau <matthieu.sozeau@inria.fr>
  2. C
    Cyprien Mangin <cyprien.mangin@m4x.org>

Maintainers

  1. M
    matthieu.sozeau@inria.fr

Sources

Coq-Equations-1.3.1-8.20.tar.gz
sha512=91c7c62ae7f78668d840bc6f14b4b387017f490215b320ba2588be957adc9c227479c54571665d64b4b3d21b16386955e4ca25c6477e05680333757b57e2d429

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.

Tags

keyword:dependent pattern-matching keyword:functional elimination category:Miscellaneous/Coq Extensions logpath:Equations date:2024-07-09

Published: 06 Sep 2024

Dependencies (2)

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

Dev Dependencies

None

Used by (10)

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

Conflicts

None