Need to record which holes are still to be solved (not counting
elaborations where there are user defined holes) and check at the end
that they are now solved.
This is for tracking locally defined names, so that we can expand their
applications to the full globally lifted name. At the moment, they don't
do anything, but since it's a change throughout the elaborator it
probably deserves its own commit.
This is for updates we make while branching in an elaborator - we don't
want to update the context immediately, because if the branch fails,
we'll need to revert, so for safety we'll note the updates we're going
to make and only complete the update when we're back at the top level.
This only searches for lambdas and locals so far, and doesn't take into
account that it shouldn't search for holes, but it does set up the basic
mechanism.
Only save the parts of terms and definitions which are needed for
typechecking and evaluation (so, for example, we don't need types for
machine generated metavariables, don't need types on lambdas, etc).
Added Core.Directory (more or less directly from Blodwen) and now
writing out TTCs from the test Main, but it's still not writing out
definitions because we're not yet making a note of the names which need
saving (this will be the defined names and any holes introduced).
Also it's clear from logging that holes/guess/constraints aren't being
cleared so this needs to be fixed next.
If an argument's type isn't known (i.e. it's still a metavariable) make
a hole for it, and delay its elaboration until the other arguments have
been elaborated.
This is to help type-directed disambiguation (so we know as much as
possible about the target type before elaborating an argument).
This checks lambdas where the type isn't immediately a pi binder. First
normalises, if that doesn't work, just guesses and unifies with the
expected type.
