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/51qi1sw5ykb1nh0g393848ia8a5npaz4-agda-ial-1.5.0.drv | ||
mips64el-linux | /gnu/store/c6pilyhwcqybwm3i2jn2c8hkg8saxslr-agda-ial-1.5.0.drv | ||
i686-linux | /gnu/store/h36yz1s2gg49c2j9564i967jgks52gpv-agda-ial-1.5.0.drv | ||
i586-gnu | /gnu/store/aqk2dspkqrkymd5f6b48624viyzs9a1c-agda-ial-1.5.0.drv | ||
armhf-linux | /gnu/store/abxyj56cp7fszr63w3j86hwly8d7bgng-agda-ial-1.5.0.drv | ||
aarch64-linux | /gnu/store/q9d64hpjgafhn2lxz7k7508smdsf0a5w-agda-ial-1.5.0.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |