Agda.Interaction.BasicOps
parseExpr
parseExprIn
giveExpr
give
refine
evalInCurrent
evalInMeta
data Rewrite
normalForm
data OutputForm a b
data OutputConstraint a b
data OutputConstraint' a b
outputFormId
showComparison
getConstraints
getSolvedInteractionPoints
typeOfMetaMI
typeOfMeta
typeOfMeta'
typesOfVisibleMetas
typesOfHiddenMetas
metaHelperType
contextOfMeta
typeInCurrent
typeInMeta
withInteractionId
withMetaId
introTactic
atTopLevel
parseName
isQName
moduleContents
getRecordContents
getModuleContents
whyInScope