* Make it typecheck (previous version of game function didn't)
* Make it more readable (if instead of case over bool, explicit precondition on NewWord)
If a type class resolution fails in an unrecoverable way (i.e., it
hasn't been postponed due to missing arguments) then it won't be one of
the things we're choosing between in type-based disambiguation, so rule
it out.
Fixes#2701
Usage:
%deprecate [name] [optional reason, as a string literal]
If 'name' is used anywhere, display a warning that it is deprecated,
along with the message.
e.g. perhaps we should shortly add:
%deprecate Float "Use Double instead. Float will be removed soon."
auto implicits need to go after the arguments they refer to, because
elaboration works left to right, and until we have better rules they may
end up solving things too early if we're not careful.
Currently: Proof search will start as long as no metavariables in the
goal type correspond to positions in the data type where an argument is
in constructor form (i.e., solving by that constructor would work
trivially, thus solving the metavariable too early).
Fixes#2656
We've always said that the rules for binding names in patterns are the
same as the rules for binding names in implicits, i.e. a name beginning
with a lower case letter, not applied to anything, will be bound
implicitly, or treated as a pattern variable. This hasn't actually
always been quite true, even though it was supposed to be...
Correspondingly, added a warning for constructor names which may be
unexpectedly bound implicitly.
This patch changes the pattern binding rules so that it is the case.
Fixes#2653
If we've expanded alternatives, the term could be very big, and we'll
get the same results if we call before expanding alternatives. If we do
need to know all the names a user has written in a term, call before
expanding the alternatives.
This addresses part of the slowness identified in #2657
If a function already exists, then adding a definition will now add the
missing cases (so in general, \d in vim or corresponding commands in
other editors will now add all the necessary clauses for a covering
definition.)
Instead of stopping at the first declaration after it reaches the line
it wants, stop at the first non-pattern-match, so that it still reads
the entire definition to avoid strange totality errors. This mostly
helps the vim mode, and :addmissing.
This makes it possible to write elaborators for term languages that use
Idris's plicity information. As a test of this, the test suite now
includes a mini-implementation of a subset of Agda's reflection using
Elab.
Also improve import chasing, by only following imports in the current
source tree (so not in dependencies we happen to have the source for,
which will be part of other packages)
This still provides misleading output from the parser about what it
was expecting, but does explain what the actual problem was:
*Pkg.PParser> execout <$> runparser pPkg defaultPkg "foo.ipkg"
"package bar\n\nexecutable = \"invalid/filename\""
Failure foo.ipkg:3:32: error: a filename
must be non-empty and have no
directory
component, expected: space
executable = "invalid/filename"<EOF>
^
Using |guard| after the parser has done its work leads to unfortunate
error messages on parse failure, though:
*Pkg.PParser> execout <$> runparser pPkg defaultPkg "foo.ipkg"
"package bar\n\nexecutable = \"invalid/filename\""
Failure foo.ipkg:3:32: error: expected: space
executable = "invalid/filename"<EOF>
^
This no longer applies as of HEAD, as pointed out by @david-christiansen,
because the Prelude now includes this namespace.
Replace the advice with a tip to :browse the Tactics module to see the list of
tactics prior to entering the elab shell.
Previously, it was parsed as an iName, AKA a possibly-namespaced identifier.
This meant you could have dots in your executable's name, but no hyphens!
See: #2721: Allow dashes in package names
(https://github.com/idris-lang/Idris-dev/issues/2721)
