2 | {-
3 | The Prelude is minimal (since it is effectively part of the language
4 | specification, this seems to be desirable - we should, nevertheless, aim to
5 | provide a good selection of base libraries). A rule of thumb is that it should
6 | contain the basic functions required by almost any non-trivial program.
8 | As such, it should contain:
10 | - Anything the elaborator can desugar to (e.g. pairs, unit, =, laziness)
11 | - Basic types Bool, Nat, List, Dec, Maybe, Either
12 | - The most important utility functions: id, the, composition, etc
13 | - Interfaces for arithmetic and implementations for the primitives and
14 | basic types
15 | - Char and String manipulation
16 | - Show, Eq, Ord, and implementations for all types in the prelude
17 | - Interfaces and functions for basic proof (cong, Uninhabited, etc) --
18 | - Semigroup, Monoid
19 | - Functor, Applicative, Monad and related functions
20 | - Foldable, Traversable
21 | - Range for range syntax
22 | - Console IO and interfaces for supporting IO
24 | Everything else should be in the base libraries, and imported as required.
25 | In particular, proofs of Nat/List properties that almost never get used in
26 | practice would probably be better in base libraries.
28 | Everything should be total, unless there's a good justification for it not
29 | to be (division by zero, as a concrete example).
31 | (These guidelines will probably get revised a few times.)
32 | -}