- 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.
These should be solved after type class resolution - they are intended
as 'side conditions' that can be proved independently, so they aren't
supposed to influence resolution. Fixes#2549.
This is because we are introducing things that aren't holes, and the
application status being "complete" might block for substitution of an
introduction. This fixes a bug in the interactive prover and the
interactive elaborator where introduction only worked when precisely the
same name was provided, becuase it was incompletely substituted.
Most uses in my real code called the (Just n) variant, and this was
needlessly noisy. Now, the surface API just takes a name, and there's an
alternate version to figure out the name.
