Agda.Interaction.CommandLine

Documentation

data ExitCode a

Constructors

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 ()

The interaction loop.

continueAfter :: TCM a -> TCM (ExitCode b)

withCurrentFile :: TCM a -> TCM a

Set envCurrentPath to optInputFile.

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

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

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

The help message