Agda.Interaction.GhciTop

data State

initState

theState

data Independence

data Interaction

isIndependent

ioTCM_

ioTCM

cmd_load

cmd_load'

data Backend

cmd_compile

cmd_constraints

cmd_metas

type GoalCommand

cmd_give

cmd_refine

cmd_intro

cmd_refine_or_intro

cmd_auto

sortInteractionPoints

prettyTypeOfMeta

prettyContext

cmd_context

cmd_infer

cmd_goal_type

cmd_goal_type_context

cmd_goal_type_context_infer

showModuleContents

cmd_show_module_contents

cmd_show_module_contents_toplevel

setCommandLineOptions

data Status

status

showStatus

displayStatus

display_info'

display_info

display_infoD

takenNameStr

refreshStr

cmd_make_case

cmd_solveAll

class LowerMeta a

cmd_compute

parseAndDoAtToplevel

cmd_infer_toplevel

cmd_compute_toplevel

cmd_write_highlighting_info

tellEmacsToJumpToError

showImplicitArgs

toggleImplicitArgs

errorTitle

displayErrorAndExit

ensureFileLoaded

getCurrentFile

makeSilent

top_command'

goal_command

mkAbsolute