Now, conditionals are implemented by the compiler rather than a
library. This gives better error messages and more readable output, at
the cost of more Haskell and less Idris.
Also, boolElim is renamed to ifThenElse for consistency with other
languages that support overloading of conditional expressions (GHC
Haskell and scala-virtualized) and to reflect that things other than
Booleans will be eliminated by overloadings.
Fixes#2217 by demanding that global names in TT terms be
unambiguous. The elaborator will always produce them that way, but user
elab scripts might not, which led to confusion.
Also, disentagle 'apply' and 'fill'.
(Type* now deprecated and replaced with AnyType). If an AnyType is a
parameter of a type, the type itself must be an AnyType otherwise we
might be able to duplicate a unique thing by mistake.
Changes:
- Eff has become EffM, parameterised over (m : Type -> Type), which will
allow us to introduce new effects later, though not currently used
- Eff itself is now a collection of type synonyms which build an EffM.
It can take either one list of effects, a list of input and output
effects, or a list of effects and a function to compute output
effects; disambiguated by context
- EffT is as Eff, but takes the underlying 'm'
- Added 'sig' function for giving effect signatures.
All of the above mean we no longer need the {} syntactic sugar, though
it's still there. Old effect programs (should!) work with no or minimal
changes.
This compiles the expression and evaluates it. It will either print the
expression (if its type is an instance of Show) or run it (if its type
is IO ()), or give an error otherwise.
This causes Idris to not emit messages about "Type checking ...." while
in quiet mode, which improves the portability of tests to Windows (due
to the slash facing the other way there). It also makes tests a bit more
robust with regards to their source files changing names.
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.
