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

Agda.TypeChecking.Rules.LHS.Unify

Synopsis

Documentation

newtype Unify a

Constructors

U 

data Equality

Constructors

Equal Type Term Term 

Instances

type Sub = Map Nat Term

data UnifyState

Constructors

USt 

Fields

uniSub :: Sub
 
uniConstr :: [Equality]
 

onSub :: (Sub -> a) -> Unify a

modSub :: (Sub -> Sub) -> Unify ()

occursCheck :: Nat -> Term -> Type -> Unify ()

Includes flexible occurrences, metas need to be solved. TODO: relax? TODO: later solutions may remove flexible occurences

(|->) :: Nat -> (Term, Type) -> Unify ()

ureduce :: Term -> Unify Term

Apply the current substitution on a term and reduce to weak head normal form.

flattenSubstitution :: Substitution -> Substitution

Take a substitution  and ensure that no variables from the domain appear in the targets. The context of the targets is not changed. TODO: can this be expressed using makeSubstitution and substs?

unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm Substitution

Unify indices.

dataOrRecordType

Arguments

:: MonadTCM tcm 
=> QName

Constructor name.

-> Type 
-> tcm Type 

Given the type of a constructor application the corresponding data or record type, applied to its parameters (extracted from the given type), is returned.

Precondition: The type has to correspond to an application of the given constructor.