| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 a | Source

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 Expr | Source

actOnMeta :: [String] -> (InteractionId -> Expr -> TCM a) -> TCM a | Source

giveMeta :: [String] -> TCM () | Source

refineMeta :: [String] -> TCM () | Source

retryConstraints :: TCM () | Source

evalIn :: [String] -> TCM () | Source

parseExpr :: String -> TCM Expr | Source

evalTerm :: String -> TCM (ExitCode a) | Source

typeOf :: [String] -> TCM () | Source

typeIn :: [String] -> TCM () | Source

showContext :: [String] -> TCM () | Source

splashScreen :: String | Source

The logo that prints when Agda is started in interactive mode.

help :: [Command a] -> IO () | Source

The help message
Produced by Haddock version 2.4.2