In a small change from Idris 1, this lifts to the nearest binder or
block, so doesn't lift past an explicit "do" in particular. Blocks are:
- case branches
- if branches
- scope of local function definitions, or any binder
- do blocks
It's a big patch, but the summary is that it's okay to use a pattern in
an erased position if either:
- the pattern can also be solved by unification (this is the same as
'dot patterns' for matching on non-constructor forms)
- the argument position is detaggable w.r.t. non-erased arguments, which
means we can tell which pattern it is without pattern matching
The second case, in particular, means we can still pattern match on
proof terms which turn out to be irrelevant, especially Refl.
Fixes#178
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.
When writing to ttc, need to take the length in bytes rather than the
length in characters. Also need to write to scheme in the appropriate
format for each scheme system.
While we're at it, Idris 1 supports unicode identifiers (although we
don't encourage it :)) so this allows any characeter >127 in an
identifier.