proof-assistant-bot-0.2.0: Telegram bot for proof assistants
Safe HaskellNone
LanguageHaskell2010

Proof.Assistant.Agda

Synopsis

Documentation

callAgda :: AgdaState -> InterpreterRequest -> IO ByteString Source #

Call Agda with its state. It will parse and execute command from the InterpreterRequest.

withChat :: ChatId -> AgdaState -> IO a -> IO a Source #

Since every chat associated with its own Agda state, we need to modify TCEnv by setting envCurrentPath with an absolute path to the corresponding file.

interpretAgda :: AgdaState -> ByteString -> IO ByteString Source #

Parse user input as command and execute in Agda.

parseRequest :: ByteString -> Either ByteString (Either () AgdaCommand, ByteString) Source #

Parse command. It could be unknown command or AgdaCommand sub-command with its arguments or even expression to evaluate.