agda-prelude
所属分类：工具库
开发工具：Agda
文件大小：0KB
下载次数：0
上传日期：2022-01-14 08:02:49
上 传 者：
sh-1993
说明： Agda编程库，
(Programming library for Agda,)
文件列表:
CHANGELOG.md (348, 2023-10-04)
LICENCE (1054, 2023-10-04)
agda-prelude.agda-lib (32, 2023-10-04)
src/ (0, 2023-10-04)
src/Builtin/ (0, 2023-10-04)
src/Builtin/Coinduction.agda (108, 2023-10-04)
src/Builtin/Float.agda (2875, 2023-10-04)
src/Builtin/Reflection.agda (11475, 2023-10-04)
src/Builtin/Size.agda (94, 2023-10-04)
src/Container/ (0, 2023-10-04)
src/Container/Bag.agda (469, 2023-10-04)
src/Container/Foldable.agda (1658, 2023-10-04)
src/Container/List.agda (4088, 2023-10-04)
src/Container/List/ (0, 2023-10-04)
src/Container/List/Permutation.agda (299, 2023-10-04)
src/Container/List/Properties.agda (2341, 2023-10-04)
src/Container/Traversable.agda (2132, 2023-10-04)
src/Control/ (0, 2023-10-04)
src/Control/Monad/ (0, 2023-10-04)
src/Control/Monad/Except.agda (2104, 2023-10-04)
src/Control/Monad/Identity.agda (1263, 2023-10-04)
src/Control/Monad/Maybe.agda (1589, 2023-10-04)
src/Control/Monad/Reader.agda (2053, 2023-10-04)
src/Control/Monad/State.agda (2210, 2023-10-04)
src/Control/Monad/Transformer.agda (285, 2023-10-04)
src/Control/Monad/Writer.agda (2734, 2023-10-04)
src/Control/Monad/Zero.agda (275, 2023-10-04)
src/Control/WellFounded.agda (986, 2023-10-04)
src/Data/ (0, 2023-10-04)
src/Data/TreeRep.agda (14497, 2023-10-04)
src/Foreign/ (0, 2023-10-04)
src/Foreign/Haskell/ (0, 2023-10-04)
src/Foreign/Haskell/Types.agda (1052, 2023-10-04)
src/Numeric/ (0, 2023-10-04)
src/Numeric/Nat.agda (762, 2023-10-04)
src/Numeric/Nat/ (0, 2023-10-04)
src/Numeric/Nat/BinarySearch.agda (3621, 2023-10-04)
src/Numeric/Nat/DivMod.agda (4870, 2023-10-04)
... ...
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.
近期下载者：
相关文件：
收藏者：