The Iowa Agda Library
The goal is to provide a concrete library focused on verification examples, as opposed to mathematics. The library has a good number of theorems for booleans, natural numbers, and lists. It also has trees, tries, vectors, and rudimentary IO. A number of good ideas come from Agda's standard library.
System | Target | Derivation | Build status |
---|---|---|---|
x86_64-linux | /gnu/store/dqyzw9v7rf7k3pivvgrvd7dz5zcpyl4j-agda-ial-1.5.0.drv | ||
mips64el-linux | /gnu/store/mldm4r13mknld3rlzbd4jkhfw2nr2yqk-agda-ial-1.5.0.drv | ||
i686-linux | /gnu/store/3kfpxcmdprjxy4763nl3a1ncr4i9qgj1-agda-ial-1.5.0.drv | ||
i586-gnu | /gnu/store/44g6bkgn5831lfyqqlscrnyf2nsnx9kz-agda-ial-1.5.0.drv | ||
armhf-linux | /gnu/store/q6502hdz2phh2rh05ny77jhlnp9bc79p-agda-ial-1.5.0.drv | ||
aarch64-linux | /gnu/store/hrprrrwgkqai4p06f145s284fr8by6f9-agda-ial-1.5.0.drv |
Linter | Message | Location |
---|---|---|
derivation Report failure to compile a package to a derivation | failed to create x86_64-linux derivation: path ‘/gnu/store/2qxyaw0yj6vin0d3zh1qhywla753d7jc-agda-2.6.0.1.drv’ is not valid | |
derivation Report failure to compile a package to a derivation | failed to create i686-linux derivation: path ‘/gnu/store/imq41gd3q2767il9gq6mqh5cv44x09rf-guile-2.2.6.drv’ is not valid | |
derivation Report failure to compile a package to a derivation | failed to create armhf-linux derivation: path ‘/gnu/store/9wn798a6w534mnn4f28lglbjmib9n392-zlib-1.2.11.drv’ is not valid | |
derivation Report failure to compile a package to a derivation | failed to create aarch64-linux derivation: path ‘/gnu/store/0afbxr7962z9ci6kw840n088qsmyz8lr-guile-2.2.6.drv’ is not valid | |
derivation Report failure to compile a package to a derivation | failed to create mips64el-linux derivation: path ‘/gnu/store/aiwgcl5dppar2s8l408bshywjybsy3nd-zlib-1.2.11.drv’ is not valid |