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/xkwzj9nd5zdqx92jalkmm3sm6fax7qvb-coq-equations-1.2.3.drv | ||
x86_64-linux | i586-pc-gnu | /gnu/store/slf7r1yr5p0mxmm1q79ajycag0hify5g-coq-equations-1.2.3.drv | |
x86_64-linux | arm-linux-gnueabihf | /gnu/store/37w95yk2k2fmnc213gpqmwc0gpbfkpvf-coq-equations-1.2.3.drv | |
x86_64-linux | aarch64-linux-gnu | /gnu/store/11fipk8wnbvv5jn780rdv5rpb0wf85cx-coq-equations-1.2.3.drv | |
powerpc64le-linux | /gnu/store/q2xq51w000m5lw5isyky3v0qn6mdsjlv-coq-equations-1.2.3.drv | ||
mips64el-linux | /gnu/store/q48lm8ksqazs6c24gp88yvg8zz4071r9-coq-equations-1.2.3.drv | ||
i686-linux | /gnu/store/nlrd7rwyz4j5icnahy6ij3xj1n3pgsd2-coq-equations-1.2.3.drv | ||
i586-gnu | /gnu/store/flzmk2ygqfq8lchw60vc6hry7idfydcf-coq-equations-1.2.3.drv | ||
armhf-linux | /gnu/store/x20ixk22c6zzhclg1n28j4lgm9wnvmz2-coq-equations-1.2.3.drv | ||
aarch64-linux | /gnu/store/nd0xbqmkj9g0p5m47i1nbn5irdjlb6zl-coq-equations-1.2.3.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |