Agda-2.6.0: A dependently typed functional programming language and proof assistant

Safe HaskellNone




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.