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
compareType
leqType
coerce
coerceSize
compareLevel
compareSort
leqSort
leqLevel
equalLevel
equalLevel'
equalSort
bothAbsurd