package coq-equations
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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page