| .. |
|
Bool
|
Add some algebra implementations
|
2020-07-17 08:25:20 -05:00 |
|
Fin
|
Cut relation implicit args
|
2021-11-25 00:26:57 +00:00 |
|
IOArray
|
Add totality annotations to src and libs/{prelude, base}
|
2021-06-12 21:06:08 -05:00 |
|
List
|
[ base ] Split a list according to a decidable property (#2302)
|
2022-02-11 11:21:20 +00:00 |
|
Nat
|
[ papers ] Tychonoff (Part I) (#2332)
|
2022-02-24 11:12:53 +00:00 |
|
Primitives
|
Add totality annotations to src and libs/{prelude, base}
|
2021-06-12 21:06:08 -05:00 |
|
SnocList
|
Injective interface and its implementations (#2114)
|
2021-11-26 10:55:17 +00:00 |
|
Vect
|
[ base ] Indexing Vectors. (#1892)
|
2021-09-09 10:45:11 +01:00 |
|
Bifoldable.idr
|
[ cleanup ] Move left autos that are most likely to be passed explicitly
|
2021-10-25 13:17:03 +01:00 |
|
Bits.idr
|
[ base ] Use Fin n as index in Bits (#2192)
|
2021-12-16 18:26:52 +00:00 |
|
Bool.idr
|
Use Not instead of -> Void (#1667)
|
2021-07-13 15:32:01 +01:00 |
|
Buffer.idr
|
Add copyFile to System.File (#1797)
|
2021-08-30 15:31:37 +01:00 |
|
Colist1.idr
|
[ fix #2034 ] Productive cantor for Colist1
|
2021-10-21 16:01:02 +01:00 |
|
Colist.idr
|
[ cleanup ] Remove unused imports (#2123)
|
2021-11-18 16:47:36 +00:00 |
|
Contravariant.idr
|
[ cleanup ] Move left autos that are most likely to be passed explicitly
|
2021-10-25 13:17:03 +01:00 |
|
DPair.idr
|
[ papers ] Tychonoff (Part I) (#2332)
|
2022-02-24 11:12:53 +00:00 |
|
Either.idr
|
Injective interface and its implementations (#2114)
|
2021-11-26 10:55:17 +00:00 |
|
Fin.idr
|
[ base ] Generalise existing min-max semigroups and add monoid for Fin (#2298)
|
2022-02-01 21:24:49 +00:00 |
|
Fuel.idr
|
[ libs ] Strengthen some totality checks (#2304)
|
2022-02-03 18:41:51 +00:00 |
|
Fun.idr
|
Some cleanup was done. Changed code is mosly equivalent to the former.
|
2021-02-16 19:05:33 +00:00 |
|
IOArray.idr
|
[ cleanup ] Remove unused imports (#2123)
|
2021-11-18 16:47:36 +00:00 |
|
IORef.idr
|
Add totality annotations to src and libs/{prelude, base}
|
2021-06-12 21:06:08 -05:00 |
|
List1.idr
|
[ new ] A couple of nearly trivial proofs about list length. (#2311)
|
2022-02-07 17:51:04 +00:00 |
|
List.idr
|
[ fix ] Literate things (#2312)
|
2022-02-18 11:29:52 +00:00 |
|
Maybe.idr
|
Injective interface and its implementations (#2114)
|
2021-11-26 10:55:17 +00:00 |
|
Morphisms.idr
|
[ breaking ] remove parsing of dangling binders (#1711)
|
2021-08-10 19:24:32 +01:00 |
|
Nat.idr
|
[ libs ] Strengthen some totality checks (#2304)
|
2022-02-03 18:41:51 +00:00 |
|
Ref.idr
|
Add totality annotations to src and libs/{prelude, base}
|
2021-06-12 21:06:08 -05:00 |
|
Rel.idr
|
Add totality annotations to src and libs/{prelude, base}
|
2021-06-12 21:06:08 -05:00 |
|
Singleton.idr
|
Add Singleton type
|
2022-01-19 14:22:40 +00:00 |
|
SnocList.idr
|
[ fix ] Literate things (#2312)
|
2022-02-18 11:29:52 +00:00 |
|
So.idr
|
[ fix #899 ] Be careful when generating an impossible LHS (#1081)
|
2021-02-22 09:53:30 +00:00 |
|
Stream.idr
|
[ fix #2034 ] Productive cantor for Colist1
|
2021-10-21 16:01:02 +01:00 |
|
String.idr
|
[ libs ] Strengthen some totality checks (#2304)
|
2022-02-03 18:41:51 +00:00 |
|
These.idr
|
[ base ] swap for these
|
2021-10-17 16:57:04 +01:00 |
|
Vect.idr
|
[ refactor ] Abstract Prelude.elem to work with all Foldables (#2294)
|
2022-02-01 21:34:29 +00:00 |
|
Zippable.idr
|
Make zip infixr 6
|
2021-02-23 10:54:28 +00:00 |
