Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.CommandLine.CommandLine
Synopsis
data ExitCode a
= Continue
| ContinueIn TCEnv
| Return a
type Command a = (String, [String] -> TCM (ExitCode a))
matchCommand :: String -> [Command a] -> Either [String] ([String] -> TCM (ExitCode a))
interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM a
interactionLoop :: TCM (Maybe Interface) -> IM ()
continueAfter :: TCM a -> TCM (ExitCode b)
loadFile :: TCM () -> [String] -> TCM ()
showConstraints :: [String] -> TCM ()
showMetas :: [String] -> TCM ()
showScope :: TCM ()
metaParseExpr :: InteractionId -> String -> TCM Expr
actOnMeta :: [String] -> (InteractionId -> Expr -> TCM a) -> TCM a
giveMeta :: [String] -> TCM ()
refineMeta :: [String] -> TCM ()
retryConstraints :: TCM ()
evalIn :: [String] -> TCM ()
parseExpr :: String -> TCM Expr
evalTerm :: String -> TCM (ExitCode a)
typeOf :: [String] -> TCM ()
typeIn :: [String] -> TCM ()
showContext :: [String] -> TCM ()
splashScreen :: String
help :: [Command a] -> IO ()
Documentation
data ExitCode a Source
Constructors
Continue
ContinueIn TCEnv
Return a
type Command a = (String, [String] -> TCM (ExitCode a))Source
matchCommand :: String -> [Command a] -> Either [String] ([String] -> TCM (ExitCode a))Source
interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM aSource
interactionLoop :: TCM (Maybe Interface) -> IM ()Source
The interaction loop.
continueAfter :: TCM a -> TCM (ExitCode b)Source
loadFile :: TCM () -> [String] -> TCM ()Source
showConstraints :: [String] -> TCM ()Source
showMetas :: [String] -> TCM ()Source
showScope :: TCM ()Source
metaParseExpr :: InteractionId -> String -> TCM ExprSource
actOnMeta :: [String] -> (InteractionId -> Expr -> TCM a) -> TCM aSource
giveMeta :: [String] -> TCM ()Source
refineMeta :: [String] -> TCM ()Source
retryConstraints :: TCM ()Source
evalIn :: [String] -> TCM ()Source
parseExpr :: String -> TCM ExprSource
evalTerm :: String -> TCM (ExitCode a)Source
typeOf :: [String] -> TCM ()Source
typeIn :: [String] -> TCM ()Source
showContext :: [String] -> TCM ()Source
splashScreen :: StringSource
The logo that prints when Agda is started in interactive mode.
help :: [Command a] -> IO ()Source
The help message
Produced by Haddock version 2.6.1