Documentation

A candidate solution for an instance meta is a term with its type.

initializeIFSMeta s t generates an instance meta of type t with suggested name s.

findInScope m (v,a)s tries to instantiate on of the types as of the candidate terms vs to the type t of the metavariable m. If successful, meta m is solved with the instantiation of v. If unsuccessful, the constraint is regenerated, with possibly reduced candidate set.

Result says whether we need to add constraint, and if so, the set of remaining candidates.

Given a meta m of type t and a list of candidates cands, checkCandidates m t cands returns a refined list of valid candidates.

To preserve the invariant that a constructor is not applied to its parameter arguments, we explicitly check whether function term we are applying to arguments is a unapplied constructor. In this case we drop the first conPars arguments. See Issue670a. Andreas, 2013-11-07 Also do this for projections, see Issue670b.

Attempt to solve irrelevant metas by instance search.