Agda.Auto.Typecheck
tcExp
getDatatype
constructorImpossible
unequals
unequal
traversePi
tcargs
addend
copyarg
type HNNBlks o
noblks
addblk
hnn
hnn_blks
hnn_checkstep
hnn'
hnb
data HNRes o
hnc
hnarglist
getNArgs
getAllArgs
data PEval o
iotastep
noiotastep
noiotastep_term
data CMode o
data CMFlex o
comp'
checkeliminand
maybeor
iotapossmeta
meta_not_constructor
calcEqRState
pickid
tcSearch