Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.InstanceArguments

Synopsis

Documentation

findInstance :: MetaId -> Maybe [Candidate] -> TCM () Source #

findInstance 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. The list of candidates is equal to Nothing when the type of the meta wasn't known when the constraint was generated. In that case, try to find its type again.

getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate]) Source #

Entry point for tcGetInstances primitive