Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Rules.LHS.Unify.Types

Synopsis

Documentation

data Equality Source #

Constructors

Equal 

Fields

data UnifyState Source #

Constructors

UState 

Fields

Instances

Instances details
PrettyTCM UnifyState Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Reduce UnifyState Source #

Don't ever reduce the whole varTel, as it will destroy readability of the context in interactive editing! To make sure this insight is not lost, the following dummy instance should prevent a proper Reduce instance for UnifyState.

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Show UnifyState Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

getVarType :: Int -> UnifyState -> Dom Type Source #

Get the type of the i'th variable in the given state

getEquality :: Int -> UnifyState -> Equality Source #

Get the k'th equality in the given state. The left- and right-hand sides of the equality live in the varTel telescope, and the type of the equality lives in the varTel++eqTel telescope

getEqualityUnraised :: Int -> UnifyState -> Equality Source #

As getEquality, but with the unraised type

solveVar Source #

Arguments

:: Int

Index k

-> DeBruijnPattern

Solution u

-> UnifyState 
-> Maybe (UnifyState, PatternSubstitution) 

Instantiate the k'th variable with the given value. Returns Nothing if there is a cycle.

dropAt :: Int -> [a] -> [a] Source #

solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution) Source #

Solve the k'th equation with the given value, which can depend on regular variables but not on other equation variables.

data UnifyStep Source #

Instances

Instances details
PrettyTCM UnifyStep Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Show UnifyStep Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

type UnifyLog' = DList (UnifyLogEntry, UnifyState) Source #

This variant of UnifyLog is used to ensure that tell is not expensive.