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.
AboutProgramming library for Agda
Resources License Stars Watchers ForksYou can’t perform that action at this time.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4