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/91albgwhwipbc9pph6hzpd8ggpjn289j-agda-ial-1.5.0.drv | ||
| mips64el-linux | /gnu/store/pixn2p31haglxb51makvf1j4lq7nh9n6-agda-ial-1.5.0.drv | ||
| i686-linux | /gnu/store/cczb7vvrdgynp2q96sjb8h6fbgl5l11s-agda-ial-1.5.0.drv | ||
| i586-gnu | /gnu/store/kf0lchvd8yksi7h0nvcq28xrbv9a0krd-agda-ial-1.5.0.drv | ||
| armhf-linux | /gnu/store/cqznfp8dy1ic2nknpr4brr7cb77hg6jb-agda-ial-1.5.0.drv | ||
| aarch64-linux | /gnu/store/z94vpxvggwn8qn1j0gwch8v58vzc1mp3-agda-ial-1.5.0.drv |
| Linter | Message | Location |
|---|---|---|
| No lint warnings ✓ | ||