Agda.TypeChecking.Conversion

tryConversion

tryConversion'

sameVars

intersectVars

equalTerm

equalAtom

equalType

convError

compareTerm

unifyPointers

assignE

compareTermDir

compareTerm'

compareTel

etaInequal

compareAtomDir

compareAtom

compareRelevance

compareElims

compareIrrelevant

compareWithPol

polFromCmp

compareArgs

Types

compareType

leqType

coerce

coerceSize

Sorts and levels

compareLevel

compareSort

leqSort

leqLevel

equalLevel

equalLevel'

equalSort

Definitions

bothAbsurd