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/16h8y3gbrjjhis7lnzzslggmafaza42c-agda-ial-1.5.0.drv | ||
| mips64el-linux | /gnu/store/kwdd5q49r6avam7p2h57xbnflxggy1cg-agda-ial-1.5.0.drv | ||
| i686-linux | /gnu/store/dyq3ly7kw0ww6wjy0kvdlzn2nchlq1g5-agda-ial-1.5.0.drv | ||
| armhf-linux | /gnu/store/m10b45i1pvqa520w7yc88614wvkbf0zr-agda-ial-1.5.0.drv | ||
| aarch64-linux | /gnu/store/n9s79ihrqmh3rn2k61yw8fjvvpd0miqa-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 |