Agda.Auto.Convert
norm
type O
data TMode
type MapS a b
initMapS
popMapS
data S
type TOM
tomy
getConst
getdfv
getMeta
getEqs
copatternsNotImplemented
tomyClauses
tomyClause
tomyPat
tomyBody
weaken
weakens
tomyType
tomyExp
tomyExps
tomyIneq
fmType
fmExp
fmExps
fmLevel
cnvh
icnvh
frommy
frommyType
frommyExp
frommyExps
abslamvarname
modifyAbstractExpr
modifyAbstractClause
constructPats
frommyClause
contains_constructor
etaContractBody
freeIn
negtype
findClauseDeep
matchType