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

Proof.Assistant.Arend

Synopsis

Documentation

callArend :: InterpreterState ArendSettings -> InterpreterRequest -> IO ByteString Source #

Call Arend typechecker as CLI application. It prepares the CLI command, executes it and waits for response.

setArendProject :: ArendSettings -> InterpreterRequest -> IO FilePath Source #

Arend requires a project for every file to typecheck. It reads project configuration, finds all files in a project directory and tries to typecheck all of them.

Since we need to isolate different chats from each other we need to ensure that every chat has its own project. And every project has its own configuration.

As result, project directory will be created, set and returned.