Inspired by the request from Kevin Meredith in the Idris mailing list for an
implementation of removeElem [1]. This borrows directly from the existing work
in the List implementation and the work in 'Type-Driven Development with Idris'
by Edwin Brady.
[1]: https://groups.google.com/d/msg/idris-lang/UKhvTKS6TfE/MEK9akzYBwAJ
This module defines the interface `Zippable (t : Type -> Type)`, which
abstracts `zipWith` and related operations into an interface.
Included are implementations of Zippable for List, Stream, and Vect, in
addition to generalizations for Maybe and Either.
Sadly we haven't be good at keeping the list of contributors up-to-date.
This fix takes the unique list fo contributors from the git logs, and
updated the list in CONTRIBUTORS. There may be a duplication of contributors
whose usernames couldn't be resolved to proper names. Duplicate names were
remove in the first place.
* change instance to implementation in string literal
* change instance to implementation in docs
* replace code level instance symbol with implementation
Totality checker incorrectly reported some partial functions with complex
arguments (data constructors inside other data constructors) as total.
For example, these functions were considered total:
h : (Bool, Bool) -> Bool
h (True, x) = True
h (y, True) = True
data PP : Type where
MkPP : Int -> PP
f : PP -> Bool
f (MkPP 0) = True
f (MkPP 1) = True
f (MkPP 2) = True
This commit fixes this and now such functions are reported as partial.
To fix this we generate more clauses which cover more possible cases.
If a candidate case fails with a 'recoverable' unification error (i.e.
one which could be fixed by allowing more reduction somewhere) then it
should be considered valid for coverage checking purposes.
Fixes#1069 (and possibly some others, not checked yet!)
(There is, I think a better fix, involving better generation of
candidate cases, which I will leave for another time)
