Agda.TypeChecking.Unquote
agdaTermType
agdaTypeType
qNameType
data Dirty
type UnquoteState
type UnquoteM
type UnquoteRes a
unpackUnquoteM
packUnquoteM
runUnquoteM
liftU
liftU1
liftU2
inOriginalContext
isCon
isDef
reduceQuotedTerm
class Unquote a
unquoteH
unquoteN
choice
ensureDef
ensureCon
pickName
unquoteString
unquoteNString
data ErrorPart
getCurrentPath
unquoteTCM
evalTCM