Safe Haskell	None
Language	Haskell2010

Proof.Assistant.State

Synopsis

data InterpreterState settings = InterpreterState {
- settings :: !settings
- input :: !(TBQueue InterpreterRequest)
}
newInterpreterState :: forall settings. ToInterpreterState settings => settings -> IO (InterpreterState settings)

Documentation

data InterpreterState settings Source #

Simple state with settings and queue as communication model between bot and backend.

Constructors

InterpreterState
Fields settings :: !settings input :: !(TBQueue InterpreterRequest)

Instances

Instances details

Interpreter InternalState InternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: InternalState -> InterpreterRequest -> IO ByteString Source # getSettings :: InternalState -> InterpreterState InternalInterpreterSettings Source #
Interpreter ExternalState ExternalInterpreterSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: ExternalState -> InterpreterRequest -> IO ByteString Source # getSettings :: ExternalState -> InterpreterState ExternalInterpreterSettings Source #
Interpreter (InterpreterState IdrisSettings) IdrisSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: InterpreterState IdrisSettings -> InterpreterRequest -> IO ByteString Source # getSettings :: InterpreterState IdrisSettings -> InterpreterState IdrisSettings Source #
Interpreter (InterpreterState ArendSettings) ArendSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: InterpreterState ArendSettings -> InterpreterRequest -> IO ByteString Source # getSettings :: InterpreterState ArendSettings -> InterpreterState ArendSettings Source #
Interpreter (InterpreterState LeanSettings) LeanSettings Source #
Instance details Defined in Proof.Assistant.Interpreter Methods interpretSafe :: InterpreterState LeanSettings -> InterpreterRequest -> IO ByteString Source # getSettings :: InterpreterState LeanSettings -> InterpreterState LeanSettings Source #

newInterpreterState :: forall settings. ToInterpreterState settings => settings -> IO (InterpreterState settings) Source #

Initialise a state based on its settings.