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

Proof.Assistant.Bot

Synopsis

Documentation

type Model = BotState Source #

Telegram Model.

data Action Source #

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 Source #

Supported backends.

Constructors

Agda 
Arend 
Idris 
Coq 
Lean 
Rzk 

proofAssistantBot :: Model -> BotApp Model Action Source #

Initiate bot app based on a Model.

updateToAction :: Model -> Update -> Maybe Action Source #

How to handle updates from Telegram.

handleAction :: Action -> Model -> Eff Action Model Source #

How to handle actions after parsing updates.

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

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

runTelegramBot :: Model -> IO () Source #

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

run :: IO () Source #

Main function.