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

Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.CommandLine

Synopsis

Documentation

data ExitCode a Source #

Constructors

Continue 
ContinueIn TCEnv 
Return a 

type Command a = (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.

withCurrentFile :: TCM a -> TCM a Source #

Set envCurrentPath to optInputFile.

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

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

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

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

typeIn :: [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