package coq-equations

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

Install

Dune Dependency

Authors

Maintainers

Sources

v1.0.tar.gz
md5=66ed25baaf876b63e2798228181ada46

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: 17 Dec 2017

Dependencies (2)

  1. coq >= "8.6" & < "8.7"
  2. ocaml

Dev Dependencies

None

Used by (2)

  1. coq-pil
  2. coq-vlsm >= "1.2"

Conflicts

None

Rocq

Interactive Theorem Prover