package coq-equations

  1. Overview
  2. Homepage

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: 16 Jun 2018

Dependencies (2)

  1. coq >= "8.8" & < "8.9"
  2. ocaml

Dev Dependencies

None

Used by (2)

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

Conflicts

None

Rocq

Interactive Theorem Prover