Safe Haskell | None |
---|
- 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)]Source
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 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.
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.
solveMetaIfIrrelevant :: MetaId -> TCM ()Source