HERMIT.Shell.Types
data QueryFun
message
performQuery
ppWholeProgram
type TagName
data VersionCmd
data CLException
abort
resume
continue
rethrowCLE
rethrowPE
data CLT m a
type CLMonad m
runCLT
clm2clt
clm
pluginM
data CommandLineState
type PathStack
data ProofTodo
data Safety
filterSafety
cl_corelint
setCoreLint
cl_cursor
setCursor
cl_diffonly
setDiffOnly
cl_failhard
setFailHard
cl_kernel
cl_kernel_env
cl_pretty
setPretty
cl_pretty_opts
setPrettyOpts
cl_render
mkCLS
getTermDimensions
data CLSBox
type ScriptName
tick
cl_putStr
cl_putStrLn
isRunningScript
setRunningScript
putStrToConsole
pathStack2Path
data Direction
pathStackToLens
getPathStack
getFocusPath
addFocusT
addFocusR
addAST
modifyLocalPath
requireDifferent
copyPathStack
copyProofStack
pushProofStack
popProofStack
currentLemma
announceProven
announceUnprovens
getProofStack
getProofStackEmpty
fixWindow
showWindow
printLemma
queryInFocus
inProofFocusT
inProofFocusR
withLemmasInScope
queryInContext