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

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

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

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

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

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

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

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

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

structure Lean.Server.RequestCancellation : Type

def Lean.Server.RequestCancellation.requestCancelled : RequestCancellation

@[reducible, inline]

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

@[reducible, inline]

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

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

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

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

def Lean.Server.CancellableM.checkCancelled : CancellableM Unit

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

@[instance_reducible]

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

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