proof-assistant-bot-0.2.0: Telegram bot for proof assistants

Index

$sel:agda:InterpretersSettingsProof.Assistant.Settings
$sel:allocations:InternalInterpreterSettingsProof.Assistant.Settings
$sel:arend:InterpretersSettingsProof.Assistant.Settings
$sel:arendModuleName:ArendSettingsProof.Assistant.Settings
$sel:arendRootProjectDir:ArendSettingsProof.Assistant.Settings
$sel:arendYamlContent:ArendSettingsProof.Assistant.Settings
$sel:arendYamlFilename:ArendSettingsProof.Assistant.Settings
$sel:args:ExternalInterpreterSettingsProof.Assistant.Settings
$sel:botName:SettingsProof.Assistant.Settings
$sel:botToken:SettingsProof.Assistant.Settings
$sel:coq:InterpretersSettingsProof.Assistant.Settings
$sel:cpuTime:ResourceSettingsProof.Assistant.Settings
$sel:dataSize:ResourceSettingsProof.Assistant.Settings
$sel:executable:ExternalInterpreterSettingsProof.Assistant.Settings
$sel:externalArend:ArendSettingsProof.Assistant.Settings
$sel:externalLean:LeanSettingsProof.Assistant.Settings
$sel:fileExtension:ExternalInterpreterSettingsProof.Assistant.Settings
$sel:fileSize:ResourceSettingsProof.Assistant.Settings
$sel:hard:LimitProof.Assistant.Settings
$sel:help:SettingsProof.Assistant.Settings
$sel:helpMessages:SettingsProof.Assistant.Settings
$sel:idris:InterpretersSettingsProof.Assistant.Settings
$sel:inputSize:ExternalInterpreterSettingsProof.Assistant.Settings
$sel:inputSize:InternalInterpreterSettingsProof.Assistant.Settings
$sel:internal:AgdaSettingsProof.Assistant.Settings
$sel:interpretersSettings:SettingsProof.Assistant.Settings
$sel:lean:InterpretersSettingsProof.Assistant.Settings
$sel:openFiles:ResourceSettingsProof.Assistant.Settings
$sel:outputSize:SettingsProof.Assistant.Settings
$sel:priority:ExternalInterpreterSettingsProof.Assistant.Settings
$sel:projectDir:LeanSettingsProof.Assistant.Settings
$sel:resources:ExternalInterpreterSettingsProof.Assistant.Settings
$sel:rzk:InterpretersSettingsProof.Assistant.Settings
$sel:soft:LimitProof.Assistant.Settings
$sel:sourceFileExtension:InternalInterpreterSettingsProof.Assistant.Settings
$sel:sourceFilePrefix:InternalInterpreterSettingsProof.Assistant.Settings
$sel:tempFilePrefix:ExternalInterpreterSettingsProof.Assistant.Settings
$sel:time:ExternalInterpreterSettingsProof.Assistant.Settings
$sel:timeout:InternalInterpreterSettingsProof.Assistant.Settings
$sel:totalMemory:ResourceSettingsProof.Assistant.Settings
$sel:version:SettingsProof.Assistant.Settings
ActionProof.Assistant.Bot
actOnMetaAgda.Interaction.Command.Internal.Parser
AgdaProof.Assistant.Bot
agdaProof.Assistant.Transport
AgdaCommandAgda.Interaction.Command
agdaEnvRefAgda.Interaction.State
AgdaSettings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
AgdaState 
1 (Type/Class)Agda.Interaction.State
2 (Data Constructor)Agda.Interaction.State
agdaStateRefAgda.Interaction.State
ArendProof.Assistant.Bot
arendProof.Assistant.Transport
ArendSettings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
asyncWaitProof.Assistant.Helpers
BackendProof.Assistant.Bot
botSettingsProof.Assistant.Transport
BotState 
1 (Type/Class)Proof.Assistant.Transport
2 (Data Constructor)Proof.Assistant.Transport
bsToTextProof.Assistant.Helpers
CallProof.Assistant.Bot
callAgdaProof.Assistant.Agda
callArendProof.Assistant.Arend
callExternalInterpreterProof.Assistant.Interpreter
callIdris2Proof.Assistant.Idris
callLeanProof.Assistant.Lean
callRzkProof.Assistant.Rzk
catchAgdaErrorAgda.Interaction.State
chatIdToStringProof.Assistant.RefreshFile
checkFileAgda.Interaction.Command.Reload
chooseCommand 
1 (Function)Idris.Interaction.Command
2 (Function)Agda.Interaction.Command
CmdArgs 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
ConstraintsAgda.Interaction.Command
ContextAgda.Interaction.Command
CoqProof.Assistant.Bot
coqProof.Assistant.Transport
DebugProof.Assistant.Bot
dropCommandProof.Assistant.Helpers
dropSubCommandProof.Assistant.Helpers
EvalAgda.Interaction.Command
evalInAgda.Interaction.Command.EvalIn
evalTermAgda.Interaction.Command.EvalTerm
Executable 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
ExternalInterpreterSettings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
ExternalStateProof.Assistant.Transport
fromBSProof.Assistant.Helpers
getQueueSizeProof.Assistant.Settings
getSettingsProof.Assistant.Interpreter
getTempFilePathProof.Assistant.RefreshFile
GiveAgda.Interaction.Command
giveMetaAgda.Interaction.Command.GiveMeta
handleActionProof.Assistant.Bot
handleErrorMaybeProof.Assistant.Helpers
Help 
1 (Data Constructor)Idris.Interaction.Command
2 (Data Constructor)Agda.Interaction.Command
3 (Data Constructor)Proof.Assistant.Bot
IdrisProof.Assistant.Bot
idrisProof.Assistant.Transport
IdrisCommandIdris.Interaction.Command
IdrisSettings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
inputProof.Assistant.State
InternalInterpreterSettings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
InternalStateProof.Assistant.Transport
interpretAgdaProof.Assistant.Agda
InterpreterProof.Assistant.Interpreter
InterpreterRequest 
1 (Type/Class)Proof.Assistant.Request
2 (Data Constructor)Proof.Assistant.Request
interpreterRequestMessageProof.Assistant.Request
interpreterRequestTelegramChatIdProof.Assistant.Request
interpreterRequestTelegramMessageIdProof.Assistant.Request
InterpreterResponse 
1 (Type/Class)Proof.Assistant.Response
2 (Data Constructor)Proof.Assistant.Response
interpreterResponseResponseProof.Assistant.Response
interpreterResponseTelegramChatIdProof.Assistant.Response
interpreterResponseTelegramMessageIdProof.Assistant.Response
Interpreters 
1 (Type/Class)Proof.Assistant.Transport
2 (Data Constructor)Proof.Assistant.Transport
interpretersProof.Assistant.Transport
InterpretersSettings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
InterpreterState 
1 (Type/Class)Proof.Assistant.State
2 (Data Constructor)Proof.Assistant.State
interpreterStateAgda.Interaction.State
interpretSafeProof.Assistant.Interpreter
LeanProof.Assistant.Bot
leanProof.Assistant.Transport
LeanSettings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
Limit 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
Load 
1 (Data Constructor)Idris.Interaction.Command
2 (Data Constructor)Agda.Interaction.Command
loadDefaultSettingsProof.Assistant.Settings
loadSettingsProof.Assistant.Settings
makeLimitsProof.Assistant.ResourceLimit
makeResourceLimitsProof.Assistant.ResourceLimit
makeTelegramResponseProof.Assistant.Response
makeVersionProof.Assistant.Version
matchSupported 
1 (Function)Idris.Interaction.Command
2 (Function)Agda.Interaction.Command
MetaAgda.Interaction.Command
metaParseExprAgda.Interaction.Command.Internal.Parser
ModelProof.Assistant.Bot
newAgdaStateAgda.Interaction.State
newBotStateProof.Assistant.Transport
newInterpretersProof.Assistant.Transport
newInterpreterStateProof.Assistant.State
outputProof.Assistant.Transport
Packages 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
parseExprAgda.Interaction.Command.Internal.Parser
parseRequest 
1 (Function)Proof.Assistant.Idris
2 (Function)Proof.Assistant.Agda
Priority 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
processErrorProof.Assistant.Helpers
proofAssistantBotProof.Assistant.Bot
proofAssistantBotVersionProof.Assistant.Version
readInputProof.Assistant.Transport
readMAgda.Interaction.Command.Internal.Parser
readOutputProof.Assistant.Transport
readTCEnvAgda.Interaction.State
readTCStateAgda.Interaction.State
RefineAgda.Interaction.Command
refineMetaAgda.Interaction.Command.RefineMeta
refreshTmpFileProof.Assistant.RefreshFile
ReloadAgda.Interaction.Command
reloadAgda.Interaction.Command.Reload
ResourceSettings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
retryConstraintsAgda.Interaction.Command.RetryConstraints
runProof.Assistant.Bot
runAgdaAgda.Interaction.State
runInterpreterProof.Assistant.Interpreter
runProcessIdris.Interaction.Command
runTelegramBotProof.Assistant.Bot
RzkProof.Assistant.Bot
rzkProof.Assistant.Transport
rzkVersionProof.Assistant.Version
ScopeAgda.Interaction.Command
SendBackProof.Assistant.Bot
sendResponseBackProof.Assistant.Bot
setArendProjectProof.Assistant.Arend
setEnvAgda.Interaction.State
setLimitsProof.Assistant.ResourceLimit
setPriorityProof.Assistant.ResourceLimit
Settings 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
settingsProof.Assistant.State
showConstraintsAgda.Interaction.Command.ShowConstraints
showContextAgda.Interaction.Command.ShowContext
showMetasAgda.Interaction.Command.ShowMetas
showScopeAgda.Interaction.Command.ShowScope
storeRequestContentAgda.Interaction.Command
supportedCommands 
1 (Function)Idris.Interaction.Command
2 (Function)Agda.Interaction.Command
t2sProof.Assistant.Helpers
textResponseIdris.Interaction.Command
textToBSProof.Assistant.Helpers
Time 
1 (Type/Class)Proof.Assistant.Settings
2 (Data Constructor)Proof.Assistant.Settings
toBSProof.Assistant.Helpers
toIntProof.Assistant.Helpers
ToInterpreterStateProof.Assistant.Settings
toSendMessageRequestProof.Assistant.Response
TypeInAgda.Interaction.Command
typeInAgda.Interaction.Command.TypeIn
TypeOf 
1 (Data Constructor)Idris.Interaction.Command
2 (Data Constructor)Agda.Interaction.Command
typeOfAgda.Interaction.Command.TypeOf
updateToActionProof.Assistant.Bot
updateToRequestProof.Assistant.Request
validateProof.Assistant.RefreshFile
validateCmdIdris.Interaction.Command
VersionProof.Assistant.Bot
WakeUpAgda.Interaction.Command
withChatProof.Assistant.Agda
withResourceIdris.Interaction.Command
writeInputProof.Assistant.Transport
writeOutputProof.Assistant.Transport
writeTCEnvAgda.Interaction.State
writeTCStateAgda.Interaction.State