This is only allowed if there is a handler for all computation contexts
the program could run in. In particular, if the program is in 'Eff'
rather than 'EffT', then it is only valid for 'pure' handlers, like
State.
Note that, as a result, the effects a program can run isn't now limited
to the top level set of effects. In the case of 'pure' effects, such as
State or Rnd, I argue that this is okay. In the case of external effects
such as IO related effects, you can only add effects if the top level
context is impure. Again, I argue that this is okay - if you don't want
to add impure effects, keep the top level context generic.
Also added a test (by way of example) in effects004
This allows extra hints, as well as constructors, to guide proof search
for auto implicit arguments.
Added test proof010 which shows how this works to simulate type classes
with overlapping instances (and consequently no injectivity restriction
or assumption)
%hint only works on functions which return an instance of a data type.
Proof search exhaustively searches hints and constructors, so use with
care especially when adding lots of recursive or overlapping hints.
Primitives for head/tail/index/cons/reverse/length now all assume the
char* is UTF8 encoded. Also updated generation of literals to encode as
UTF8. Primitives are probably not as efficient as they could be (though
some of the will be used rarely)
ASCII strings will work exactly as before.
Everything I know about UTF8 encoding has been learned in the past few
hours. Therefore, this is unlikely to be the best way to do this. Please
educate me, ideally in the form of annotated Pull Requests :).
We weren't shadowing names correctly when a class was parameterised on a
single variable and one of the methods bound the same name. This almost
never happens, but leads to very odd error messages when it does.
Fixes#2026
Need to expand implicits for methods in the dictionary declarataion, but
not quite the same way as for the top level function of the same name
(i.e. need to leave out the dictionary itself).
Fixes#1975
This commit introduces:
* A new tactic "claim N TY" that introduces a new hole named N with
type TY
* A new tactic "unfocus" that moves the current hole to the bottom of
the hole stack
In the process of this and some other work, I also added comments and
docs to more of the core.
If after an application there are more implicit arguments expected, add
those arguments then re-elaborate the application - we often don't know
what these arguments will be until after elaborating the application
because the application itself may compute a type.
Fixes#1899
This patch changes the name of the machine-readable REPL syntax from
ideslave to ide-mode. The old command line options still work, but are
announced as deprecated for a while.
