Agda.TypeChecking.Conversion
mlevel
nextPolarity
sameVars
intersectVars
equalTerm
equalAtom
equalType
compareTerm
compareTerm'
compareTel
compareAtom
compareElims
compareArgs
compareType
leqType
compareSort
leqSort
leqLevel
equalLevel
equalSort