structure Lean.Server.RequestCancellationToken : Type

• cancelledByCancelRequest : IO.Ref Bool
• cancelledByEdit : IO.Ref Bool
• cancellationPromise : IO.Promise Unit

def Lean.Server.RequestCancellationToken.new : BaseIO RequestCancellationToken

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.RequestCancellationToken.cancelByCancelRequest (tk : RequestCancellationToken) : BaseIO Unit

Equations

• tk.cancelByCancelRequest = do ST.Ref.set tk.cancelledByCancelRequest true IO.Promise.resolve () tk.cancellationPromise

def Lean.Server.RequestCancellationToken.cancelByEdit (tk : RequestCancellationToken) : BaseIO Unit

Equations

• tk.cancelByEdit = do ST.Ref.set tk.cancelledByEdit true IO.Promise.resolve () tk.cancellationPromise

def Lean.Server.RequestCancellationToken.cancellationTask (tk : RequestCancellationToken) : Task Unit

Equations

• tk.cancellationTask = tk.cancellationPromise.result!

def Lean.Server.RequestCancellationToken.wasCancelledByCancelRequest (tk : RequestCancellationToken) : BaseIO Bool

Equations

• tk.wasCancelledByCancelRequest = ST.Ref.get tk.cancelledByCancelRequest

def Lean.Server.RequestCancellationToken.wasCancelledByEdit (tk : RequestCancellationToken) : BaseIO Bool

Equations

• tk.wasCancelledByEdit = ST.Ref.get tk.cancelledByEdit

structure Lean.Server.RequestCancellation : Type

def Lean.Server.RequestCancellation.requestCancelled : RequestCancellation

Equations

• Lean.Server.RequestCancellation.requestCancelled = { }

@[reducible, inline]

abbrev Lean.Server.CancellableT (m : Type → Type u_1) (α : Type) : Type u_1

Equations

• Lean.Server.CancellableT m = ReaderT Lean.Server.RequestCancellationToken (ExceptT Lean.Server.RequestCancellation m)

@[reducible, inline]

abbrev Lean.Server.CancellableM (α : Type) : Type

Equations

• Lean.Server.CancellableM = Lean.Server.CancellableT IO

def Lean.Server.CancellableT.run {m : Type → Type u_1} {α : Type} (tk : RequestCancellationToken) (x : CancellableT m α) : m (Except RequestCancellation α)

Equations

• Lean.Server.CancellableT.run tk x = x tk

def Lean.Server.CancellableM.run {α : Type} (tk : RequestCancellationToken) (x : CancellableM α) : IO (Except RequestCancellation α)

Equations

• Lean.Server.CancellableM.run tk x = Lean.Server.CancellableT.run tk x

def Lean.Server.CancellableT.checkCancelled {m : Type → Type u_1} [Monad m] [MonadLiftT BaseIO m] : CancellableT m Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.CancellableM.checkCancelled : CancellableM Unit

Equations

• Lean.Server.CancellableM.checkCancelled = Lean.Server.CancellableT.checkCancelled

class Lean.Server.MonadCancellable (m : Type → Type v) : Type v

• checkCancelled : m PUnit

instance Lean.Server.instMonadCancellableOfMonadLift (m : Type → Type u_1) (n : Type → Type u_2) [MonadLift m n] [MonadCancellable m] : MonadCancellable n

Equations

• Lean.Server.instMonadCancellableOfMonadLift m n = { checkCancelled := liftM Lean.Server.MonadCancellable.checkCancelled }

instance Lean.Server.instMonadCancellableCancellableTOfMonadOfMonadLiftTBaseIO {m : Type → Type u_1} [Monad m] [MonadLiftT BaseIO m] : MonadCancellable (CancellableT m)

Equations

• Lean.Server.instMonadCancellableCancellableTOfMonadOfMonadLiftTBaseIO = { checkCancelled := Lean.Server.CancellableT.checkCancelled }

def Lean.Server.RequestCancellation.check {m : Type → Type u_1} [MonadCancellable m] : m Unit

Equations

• Lean.Server.RequestCancellation.check = Lean.Server.MonadCancellable.checkCancelled