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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Rules.LHS.Unify

Synopsis

Documentation

type UnificationResult = UnificationResult' (Telescope, PatternSubstitution) Source

Result of unifyIndices.

data UnificationResult' a Source

Constructors

Unifies a

Unification succeeded.

NoUnify TCErr

Terms are not unifiable.

DontKnow TCErr

Some other error happened, unification got stuck.

Instances

Functor UnificationResult' Source 
Foldable UnificationResult' Source 
Traversable UnificationResult' Source 
Show a => Show (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.