Safe Haskell | None |
---|---|
Language | Haskell98 |
- type UnificationResult = UnificationResult' (Telescope, PatternSubstitution)
- data UnificationResult' a
- unifyIndices :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult
- unifyIndices_ :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm (Telescope, PatternSubstitution)
Documentation
type UnificationResult = UnificationResult' (Telescope, PatternSubstitution) Source #
Result of unifyIndices
.
data UnificationResult' a Source #
unifyIndices :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult Source #
unifyIndices_ :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm (Telescope, PatternSubstitution) Source #
Unify indices.
In unifyIndices_ flex a us vs
,
a
is the type eliminated by us
and vs
(usally the type of a constructor),
need not be reduced,
us
and vs
are the argument lists to unify,
flex
is the set of flexible (instantiable) variabes in us
and vs
.
The result is the most general unifier of us
and vs
.