Agda.Interaction.GhciTop
data
State
initState
theState
ioTCM
cmd_load
cmd_load'
cmd_compile
cmd_constraints
cmd_metas
cmd_undo
cmd_reset
type
GoalCommand
cmd_give
cmd_refine
sortInteractionPoints
prettyTypeOfMeta
prettyContext
cmd_context
cmd_infer
cmd_goal_type
cmd_goal_type_context_and
cmd_goal_type_context
cmd_goal_type_context_infer
setCommandLineOptions
displayStatus
display_info
display_infoD
response
data
Lisp
a
takenNameStr
refreshStr
cmd_make_case
cmd_solveAll
class
LowerMeta
a
cmd_compute
parseAndDoAtToplevel
cmd_infer_toplevel
cmd_compute_toplevel
tellEmacsToUpdateGoals
tellEmacsToReloadSyntaxInfo
tellEmacsToJumpToError
showImplicitArgs
toggleImplicitArgs
errorTitle
displayErrorAndExit