Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




initializeIFSMeta :: String -> Type -> TCM TermSource

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

findInScope :: MetaId -> [(Term, Type)] -> TCM ()Source

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.

applyDroppingParameters :: Term -> Args -> TCM TermSource

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.

solveIrrelevantMetas :: TCM ()Source

Attempt to solve irrelevant metas by instance search.