* contrib library unused import removal
* remove a few unused imports.
* another round of unused import removal
* another round of unused import deletion.
* another round of unused import deletion.
The prelude interfaces that have default definitions for all of
their fields are declared total so that users are forced to think
about meeting the minimal requirements for an implementation to be
valid.
* deprecate Data.Nat.Order.decideLTE
* Add properties for LTE/GTE that produce the difference.
* remove deprecated function now that it is available in the base library.
* remove two deprecated lines.
* remove module deprecated since v0.4.0
* fix prelude reference to renamed primitive.
* finish removing Data.Num.Implementations
* remove deprecated dirEntry function.
* remove deprecated fastAppend. Update CHANGELOG.
* replace fastAppend in test case
* replace fastAppend uses in compiler.
* remove new properties that weren't actually very new.
* [ breaking ] remove parsing of dangling binders
It used to be the case that
```
ID : Type -> Type
ID a = a
test : ID (a : Type) -> a -> a
test = \ a, x => x
```
and
```
head : List $ a -> Maybe a
head [] = Nothing
head (x :: _) = Just x
```
were accepted but these are now rejected because:
* `ID (a : Type) -> a -> a` is parsed as `(ID (a : Type)) -> a -> a`
* `List $ a -> Maybe a` is parsed as `List (a -> Maybe a)`
Similarly if you want to use a lambda / rewrite / let expression as
part of the last argument of an application, the use of `$` or parens
is now mandatory.
This should hopefully allow us to make progress on #1703
In the `MkFix : f (Fix f) -> Fix f` example, using `Erased` for `f`
makes the type reduce to `[__] (Fix [__]) -> Fix [__]` and because
`[__] e1 ... en` computes to `[__]`, we end up with `[__] -> Fix [__]`
which does not reference `Fix` anymore.
A few proofs have been rewritten, a few unnecessary cases cut, and
lots of unnecessary "explicit implicits" have been cut. Probably these
implicits were required when the code was initially written, and
inference has improved since then.
* Add trailing newline on non-empty list in unlines
There are several reasons to do that:
* a line in a text file is something which ends with newline,
and the last line is not special
* `unlines []` should be different from `unlines [""]`
* `unlines (a ++ b) = unlines a ++ unlines b`
* Haskell does it
* Change lines function behaviour
This has a much better behaviour with respect to proof search and
the coverage checker realising we don't need to consider the Z case
than the `Not (x = Z)` we used earlier.
