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/9xard379dy6bb7vk6cmw8i3f1g6iy3cw-agda-ial-1.5.0.drv | ||
powerpc64le-linux | /gnu/store/dva1sj9am5p6qcn51fahxzkh01yh8mmf-agda-ial-1.5.0.drv | ||
mips64el-linux | /gnu/store/asni0wyg3m8vdl1l6xg9lnc0m6ba4idw-agda-ial-1.5.0.drv | ||
i686-linux | /gnu/store/7435myl2xsb6inn5j78h17ch1xpprg43-agda-ial-1.5.0.drv | ||
i586-gnu | /gnu/store/rp1hzv742nf6bahlcn5b67fjj9cjkvl1-agda-ial-1.5.0.drv | ||
armhf-linux | /gnu/store/ncp4j71mb2c3lvpy9kbs71r7nh86ds3h-agda-ial-1.5.0.drv | ||
aarch64-linux | /gnu/store/7si5n56hyb51z3a72nmif8pihy8ld1v8-agda-ial-1.5.0.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |