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

give_gen

give_gen'

cmd_intro

cmd_refine_or_intro

cmd_auto

sortInteractionPoints

prettyTypeOfMeta

prettyContext

cmd_context

cmd_infer

cmd_goal_type

cmd_goal_type_context_and

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

showNumIId

takenNameStr

refreshStr

nameModifiers

cmd_make_case

cmd_solveAll

class LowerMeta a

preMeta

preUscore

cmd_compute

parseAndDoAtToplevel

cmd_infer_toplevel

cmd_compute_toplevel

cmd_write_highlighting_info

tellEmacsToJumpToError

showImplicitArgs

toggleImplicitArgs

errorTitle

displayErrorAndExit

infoOnException

ensureFileLoaded

getCurrentFile

makeSilent

top_command'

goal_command

mkAbsolute