If we normalise the goal type before coercion, we also need to check
against the normalised coercion type otherwise we might miss some valid
coercions. Fixes#2570
Postpone failing searches rather than giving up immediately, since more
information (e.g. type class constraints) may be available when trying
later.
Also improves error reporting of postponed searches by recording what
was being elaborated at the time.
Fixes#2456
Neg now means "Numbers with possible negative values" and the methods
which deal with negative numbrs (abs, - and negate) are now part of this
rather than Num.
This means, in particular, that - on Nat can now require a proof.
'minus' on Nat behaves as before (and the proofs use minus rather than
-).
Ran aspell over the documentation. Where there were conflicts between
American and British spelling, picked the British variant, as most of it
seemed to be written in that style. I don't really care, I'm American.
- Define a new data type to store information about records (RecordInfo)
In particular: parameters, constructor and projections
- Add a new field to IState (idris_records)
- Update record elaboration so that the elaborated record is added
to idris_records
Check for metavariable application didn't actually look for arguments,
preventing some perfectly reasonable searches from happening. Two
regression tests added (under proofsearch00x)
Under a PHidden we can't encounter new pattern variables, so make
addImpl aware of this. As a result, there's no longer any need to
qualify constant function names under a function application on the lhs.
Transform rules shouldn't be adding things to the global set of universe
constraints, since they have nothing to do with them. This turns off
universe constraints in partial evaluator generated definitions in
particular, which should not interfere with type checking of the rest of
the program.
Parameters should only be assumed to be injective if they also happen to
be type class parameters, otherwise some things will type check which
otherwise shouldn't.
This new format divides updates into various categories, and makes it
much easier to write release notes. It's also useful to order by
approximate importance (but this is mostly subjective so not sure
it's worth trying too hard to do that.)
The docs made it seem that a double-backslash was not user definable.
It turns out that it's a single backslash that's not user definable;
the docs preserved escaping from the Haskell implementation
(cf. src/Idris/ParseHelpers.hs:/invalidOperators/).
Thanks to @mietek, niklasl2, and @Melvar for pointing this out
in #idris.
