Package coq-equations @ 1.2

Synopsis

Function definition plugin for Coq

Description

Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq. It compiles everything down to eliminators for inductive types, equality and accessibility, providing a definitional extension to the Coq kernel.

Home page
https://mattam82.github.io/Coq-Equations/
Location
gnu/packages/coq.scm (line: 525, column: 2)
License

Lint warnings

LinterMessageLocation
No lint warnings