structure Lean.Server.RequestCancellationToken : Type

• cancelledByCancelRequest : IO.CancelToken
• cancelledByEdit : IO.CancelToken
• requestCancellationPromise : IO.Promise Unit
• editCancellationPromise : 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 tk.cancelledByCancelRequest.set IO.Promise.resolve () tk.requestCancellationPromise

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

Equations

• tk.cancelByEdit = do tk.cancelledByEdit.set IO.Promise.resolve () tk.editCancellationPromise

def Lean.Server.RequestCancellationToken.requestCancellationTask (tk : RequestCancellationToken) : ServerTask Unit

Equations

• tk.requestCancellationTask = { task := tk.requestCancellationPromise.resultD () }

def Lean.Server.RequestCancellationToken.editCancellationTask (tk : RequestCancellationToken) : ServerTask Unit

Equations

• tk.editCancellationTask = { task := tk.editCancellationPromise.resultD () }

def Lean.Server.RequestCancellationToken.cancellationTasks (tk : RequestCancellationToken) : List (ServerTask Unit)

Equations

• tk.cancellationTasks = [tk.requestCancellationTask, tk.editCancellationTask]

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

Equations

• tk.wasCancelledByCancelRequest = tk.cancelledByCancelRequest.isSet

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

Equations

• tk.wasCancelledByEdit = tk.cancelledByEdit.isSet

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

Equations

• tk.wasCancelled = do let __do_lift ← tk.wasCancelledByCancelRequest let __do_lift_1 ← tk.wasCancelledByEdit pure (__do_lift || __do_lift_1)

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_reducible]

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_reducible]

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