Agda.TypeChecking.Rules.LHS.Unify

data Unify a

data UnifyMayPostpone

type UnifyEnv

noPostponing

askPostpone

type UnifyOutput

emptyUOutput

data Unifiable

reportPostponing

ifClean

data Equality

type Sub

data UnifyException

data UnifyState

constructorMismatch

constructorMismatchHH

onSub

modSub

checkEqualities

checkEquality

checkEqualityHH

forceHom

addEquality

addEqualityHH

takeEqualities

occursCheck

(|->)

makeSubstitution

class UReduce t

flattenSubstitution

data UnificationResult

data HomHet a

isHom

fromHom

leftHH

rightHH

type TermHH

type TypeHH

type TelHH

type TelViewHH

absAppHH

class ApplyHH t

substHH

class SubstHH t tHH

unifyIndices_

unifyIndices

dataOrRecordType

dataOrRecordType'

dataOrRecordTypeHH

isEtaRecordTypeHH

data ShapeView a

shapeView

shapeViewHH

telViewUpToHH