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

Safe Haskell | None

Agda.TypeChecking.InstanceArguments

Synopsis

- initialIFSCandidates :: TCM [(Term, Type)]
- initializeIFSMeta :: String -> Type -> TCM Term
- findInScope :: MetaId -> [(Term, Type)] -> TCM ()
- findInScope' :: MetaId -> [(Term, Type)] -> TCM (Maybe [(Term, Type)])
- getMetaTypeInContext :: MetaId -> TCM Type
- checkCandidates :: MetaId -> Type -> [(Term, Type)] -> TCM [(Term, Type)]
- applyDroppingParameters :: Term -> Args -> TCM Term
- solveIrrelevantMetas :: TCM ()
- solveMetaIfIrrelevant :: MetaId -> TCM ()

# Documentation

initialIFSCandidates :: TCM [(Term, Type)]

initializeIFSMeta :: String -> Type -> TCM Term

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

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

`findInScope m (v,a)s` tries to instantiate on of the types `a`s of the candidate terms `v`s 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.

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

getMetaTypeInContext :: MetaId -> TCM Type

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

applyDroppingParameters :: Term -> Args -> TCM Term

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 ()

Attempt to solve irrelevant metas by instance search.

solveMetaIfIrrelevant :: MetaId -> TCM ()