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/2f0jh3c9vcpm3cf4f8rmhbay8k4i5x5h-agda-ial-1.5.0.drv | ||
| powerpc64le-linux | /gnu/store/yzykh8pyw8wc482favkvglh1000ffnq0-agda-ial-1.5.0.drv | ||
| mips64el-linux | /gnu/store/j11gx9v7vzm0hh45yhamjq4vds1s47rb-agda-ial-1.5.0.drv | ||
| i686-linux | /gnu/store/5j77k3y4j6av0s54fv9qyd598xi98rbq-agda-ial-1.5.0.drv | ||
| i586-gnu | /gnu/store/dxlmcjcfzk28z7flqlz9rgmlg2b0rq9p-agda-ial-1.5.0.drv | ||
| armhf-linux | /gnu/store/vdzhwnls4n33dqsxcwvjakgcqg89s6r7-agda-ial-1.5.0.drv | ||
| aarch64-linux | /gnu/store/mnjhvp2788q9arzapjzgk3m660ac1f36-agda-ial-1.5.0.drv |
| Linter | Message | Location |
|---|---|---|
| No lint warnings ✓ | ||