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/0zh5g5amhym4ph92f02xvfhklsvcl084-agda-ial-1.5.0.drv | ||
mips64el-linux | /gnu/store/ffxls1rxwhfyw3qlpxlcgrl0g06zjz37-agda-ial-1.5.0.drv | ||
i686-linux | /gnu/store/rxj7s9rdpy25iknjy9wh1nwrij2vx40k-agda-ial-1.5.0.drv | ||
i586-gnu | /gnu/store/imcyqwy5n3hjbyn7cqkr8mgpgys3jr6k-agda-ial-1.5.0.drv | ||
armhf-linux | /gnu/store/wawzx4n0bkfhvwc7jcgvfarxrs2r8d5r-agda-ial-1.5.0.drv | ||
aarch64-linux | /gnu/store/mgbz8dpgj1lghnx74dp58ybgv7xvl1bb-agda-ial-1.5.0.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |