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

Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.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.

withCurrentFile :: TCM a -> TCM a #

Set envCurrentPath to optInputFile.

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

showMetas :: [String] -> TCM () #

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

giveMeta :: [String] -> TCM () #

refineMeta :: [String] -> TCM () #

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

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