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/9mbqzggin98pga4va9p846zgypqagv4h-agda-ial-1.5.0.drv | ||
mips64el-linux | /gnu/store/p1ci24gl2gm4162pc4qmhnc5734yws1r-agda-ial-1.5.0.drv | ||
i686-linux | /gnu/store/fdvxm4d15mwn41xghhdm78xph1gmxyhx-agda-ial-1.5.0.drv | ||
i586-gnu | /gnu/store/hrqkyfsxj6n4x709gvg42jhq3v1m033i-agda-ial-1.5.0.drv | ||
armhf-linux | /gnu/store/gx7cxmyjkxy8x9z2awa0x1rz5d3j8a76-agda-ial-1.5.0.drv | ||
aarch64-linux | /gnu/store/klvvb7h42zsssgnb0194dw1m6kdxknsm-agda-ial-1.5.0.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |