Proof.Assistant.Bot

Documentation

type Model = BotState

Telegram Model.

data Action

Supported actions by bot.

Constructors

Call Backend InterpreterRequest

Call backend and send request to it.

SendBack InterpreterResponse

Send response back as reply.

Help InterpreterRequest

Reply with help message.

Version InterpreterRequest

Reply with version message.

Debug String

Write in STDOUT unknown input.

data Backend

Supported backends.

Constructors

Agda

Arend

Idris

Coq

Lean

Rzk

proofAssistantBot :: Model -> BotApp Model Action

Initiate bot app based on a Model.

updateToAction :: Model -> Update -> Maybe Action

How to handle updates from Telegram.

handleAction :: Action -> Model -> Eff Action Model

How to handle actions after parsing updates.

sendResponseBack :: Bool -> InterpreterResponse -> BotM ()

Helper that will try to deliver message even when Telegram failed to send it.

runTelegramBot :: Model -> IO ()

Initiate Telegram Env, Model, start Bot, start backends concurrently.

run :: IO ()

Main function.