package coq-equations
A function definition package for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.0-8.8.tar.gz
md5=eb04fd0e757d7e66a40cb55bad24f004
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: 20 Apr 2018
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page