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