This is further progress towards a metaprogramming system in a form
similar to Elaborator Reflection or Template Haskell, but trying to
avoid leaking too many implementation details of the elaborator itself.
Also include proof the tail-recursive versions are extensionally equivalent to the non-tail-recursive one
I'm a bit worried that some of those proofs came through, as
visibility modifiers should get in the way. If they cause problems at
some future point, just delete/comment them out.
This is the result of running the command:
$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +
I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
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.
See e.g. Applicative instance in Data.Vect. This allows implementations
to use implicits at run time (by default, they'd be 0 multiplicity so
erased, but it might be useful to have an index available at run time).
At the moment, the parser requires implicits to be given before
constraints. Ideally it should be possible to give them in any order.
I'll come back to this.
Lots were missing, and some were export, which should probably be public
export because the nature of Vect is that it could commonly be used in
types.
Fixes#13
This is part of what we used to have in Enum but I think it's better to
separate the two. Added implementations for Nat, and anything in
Integral/Ord/Neg, so that we get range syntax (at least when its
implemeted) for the most useful cases.
This required a small change to auto implicit search (and I'm still not
sure about this). Now search arguments right to left, because solving
later arguments may resolve earlier arguments by unification and this
can happen in particular when chasing parent interfaces (which may have
fewer parameters).
Now supports with applications on the RHS when auto implicits are
involved. Auto implicit bound names in patterns now become searches on
the rhs in a with-application (I should write this construct up properly
in a paper some time!)
