UlfNorell / Agda Prelude
Licence: mit
Programming library for Agda
Stars: ✭ 103
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.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].