Proof.Assistant.Agda

Documentation

callAgda :: AgdaState -> InterpreterRequest -> IO ByteString

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

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

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

Parse user input as command and execute in Agda.

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

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