Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.Interaction.CommandLine.CommandLine

Synopsis

Documentation

data ExitCode a

Constructors

Continue 
ContinueIn TCEnv 
Return a 

type Command a = (String, [String] -> TCM (ExitCode a))

interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM a

interactionLoop :: TCM (Maybe Interface) -> IM ()

The interaction loop.

loadFile :: TCM () -> [String] -> TCM ()

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

splashScreen :: String

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

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

The help message