The Agda standard library: version 2.0
Summary
Agda is a dependently-typed functional language that serves as both a programming language and an interactive theorem prover (ITP).
In Agda, one can formulate requirements on programs as types and build programs satisfying these requirements interactively.
The Curry-Howard correspondence allows types and programs to be seen as theorems and proofs.
We present the Agda standard library (agda-stdlib), which provides functions and mathematical concepts helpful in the development of both programs and proofs.
