| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.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)
- withCurrentFile :: TCM a -> TCM a
- 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
withCurrentFile :: TCM a -> TCM a Source #
Set envCurrentPath to optInputFile.
showConstraints :: [String] -> TCM () Source #
metaParseExpr :: InteractionId -> String -> TCM Expr Source #
refineMeta :: [String] -> TCM () Source #
retryConstraints :: TCM () Source #
showContext :: [String] -> TCM () Source #
splashScreen :: String Source #
The logo that prints when Agda is started in interactive mode.