This is an alternative to the Agda standard library that focuses more on programming and type checking time performance.

Notable features:

• Makes heavy use of instance arguments.

• Efficient decision procedures for natural number arithmetic (Tactic.Nat).

• Evidence-producing and efficient gcd and primality testing (Data.Nat.GCD and Data.Nat.Prime).

This is very much work in progress, so expect major changes. In particular the proof-side of things is very much unstructured.