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/6fq6fzjykibkgfxx652y0z8dcxanxwa4-agda-ial-1.5.0.drv | ||
powerpc64le-linux | /gnu/store/arsjhmkic08c3h8p24r4z0qccxg381m2-agda-ial-1.5.0.drv | ||
mips64el-linux | /gnu/store/mhl1762nz0a2r0d7mcrf2bymmw8vpxlh-agda-ial-1.5.0.drv | ||
i686-linux | /gnu/store/0ixq50axzw5a3x43yxrfb8r01hbqhm5v-agda-ial-1.5.0.drv | ||
i586-gnu | /gnu/store/hgyxyk2gmy8bx7y2kl0hr60nkxplhpgi-agda-ial-1.5.0.drv | ||
armhf-linux | /gnu/store/vvlrf6nb58dkfd6fbpn1727jci6a8y7k-agda-ial-1.5.0.drv | ||
aarch64-linux | /gnu/store/gjcpbbi0m91415jv0g6897h06y2ridjk-agda-ial-1.5.0.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |