Michael Morgan 33110d1cda Add head and tail to base/Data.List. ... These functions use the NonEmpty predicate type in order to prove that the operation will be valid. Implementations copied from Idris1's Prelude.List module, except without expanding the auto implicit argument.		2019-10-16 15:49:52 -07:00
..
List	Add decidable equality for List	2019-10-10 17:38:09 +01:00
Nat	Improve 'with' implementation	2019-07-08 12:55:55 +02:00
Primitives	Add Data.Primitives.Views	2019-07-08 22:11:34 +02:00
Buffer.idr	Reading/writing buffers can fail	2019-09-28 18:33:46 +01:00
Either.idr	Inclusion of Either within Base.	2019-07-18 16:32:19 +01:00
Fin.idr	Make some things public export	2019-08-21 17:44:17 +02:00
IORef.idr	Add 'base' libraries	2019-06-15 11:54:22 +01:00
List.idr	Add head and tail to base/Data.List.	2019-10-16 15:49:52 -07:00
Maybe.idr	Delay case elaboration	2019-07-02 16:53:41 +01:00
Morphisms.idr	Add Data.Morphisms to base	2019-07-18 14:46:59 +01:00
Nat.idr	Add Range interface to prelude	2019-07-11 23:38:25 +02:00
So.idr	Parse pattern matching lambda	2019-07-03 13:04:25 +01:00
Stream.idr	Add more stream functions to Data.Stream	2019-07-08 18:10:47 +02:00
Strings.idr	add 'missing' functions into base libraries	2019-07-23 09:37:48 +02:00
Vect.idr	Allow implementations to have implicits given	2019-10-13 12:32:07 +01:00