Proof.Assistant.Arend

Documentation

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

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

setArendProject :: ArendSettings -> InterpreterRequest -> IO FilePath

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.