Function definition plugin for Coq
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.
| System | Target | Derivation | Build status |
|---|---|---|---|
| x86_64-linux | /gnu/store/jihxqpy26k7gvwawxjbl5bf5lgg8damr-coq-equations-1.2.1.drv | ||
| mips64el-linux | /gnu/store/26cbyy7lsam6cb8kxz20f7zglw8kgsg3-coq-equations-1.2.1.drv | ||
| i686-linux | /gnu/store/zwq8bmrbd3hdgfwnqw3dz61armmphc91-coq-equations-1.2.1.drv | ||
| armhf-linux | /gnu/store/y1nrrijkavj4z909slwxdcym8fz3f3iv-coq-equations-1.2.1.drv | ||
| aarch64-linux | /gnu/store/n598djxw07l83360rabcwyndvy0fz9mq-coq-equations-1.2.1.drv |
| Linter | Message | Location |
|---|---|---|
| No lint warnings ✓ | ||