Executables now get built and deleted. Install doesn't do anything with
the executable, and --clean only deletes the executable itself (not any
support files or libraries that might also have been generated in the
exec directory)
The names weren't fully explicit in the elaborator, so ambiguity
resolution wasn't able to take advantage of type-directed pruning. Now
they're explicit (but hard-coded, which we should fix later...) so they
can be resolved more easily.
Do two passes through delayed elaborators (it's impossible to predict
dependency order). Possibly this should keep going as long as it's
making progress? I'll consider that later.
We can work out what it should be since each case is supposed to have
the same type, so we can look ahead to the alternatives. This way, we
don't have to rely on the scrutinee alone to calculate the type of the
case block. (Idris 1 does this too but I've only just encountered the
need for it in Idris 2 now!)
Explaining how to write the most basic Idris bindings for readline,
taking account of how to allocate Strings in the completion callback.
Also adds the basic API as a sample, which can be used as a starting
point for other packages containing C bindings.
That's most of it now - just missing a section on multiplicities, and a
section on the differences from Idris 1.
Ideally, there should also be a much more gentle introduction (basically
doing the same as the first 3 chapters of TypeDD in Idris). But that's
for some other time...
These are still to be updated (as noted in the files), but it needs
doing before any kind of preliminary release. Plan is to refresh the
tutorial and make sure samples work again, then write a more
comprehensive document explaining changes since Idris 1.
This is an initial copy and refinement of the existing documentation for packaging.
This commit also starts the Idris2 reference documentation, in which we can start documenting the language proper. Maybe we should include the contents of `Notes` here, but that is a question for later.
