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/47iqibcl5zv4a4rnjs2jbr5yzdg5g9f9-agda-ial-1.5.0.drv | ||
powerpc64le-linux | /gnu/store/6jc1zvx4bv2gpy3lffsgn9rkzp1gv0j0-agda-ial-1.5.0.drv | ||
mips64el-linux | /gnu/store/9y51dg893py2hkixxcl5yzcaj7pilhc8-agda-ial-1.5.0.drv | ||
i686-linux | /gnu/store/ww5rgbmbb01xz9h0w9lkw8gy3rzk4w7i-agda-ial-1.5.0.drv | ||
i586-gnu | /gnu/store/8nvmkpdvxipp9n0h9d83cxjwl5ry9zwn-agda-ial-1.5.0.drv | ||
armhf-linux | /gnu/store/1lya6zfybdwypwx14vh84zd22pvhps5r-agda-ial-1.5.0.drv | ||
aarch64-linux | /gnu/store/vksbdifpc7hj37g6rlb5k1m73l7yn25i-agda-ial-1.5.0.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |