structure Control.Monad.Trans.Resource.ReleaseKey : Type

Opaque key for a registered cleanup action. Single-use: calling release twice is a no-op.

• id : Nat

def Control.Monad.Trans.Resource.ResourceT (m : Type → Type) (α : Type) : Type

Resource management monad transformer. $$\text{ResourceT}\ m\ \alpha = \text{IO.Ref CleanupMap} \to m\ \alpha$$

Equations

• Control.Monad.Trans.Resource.ResourceT m α = (IO.Ref Control.Monad.Trans.Resource.CleanupMap✝ → m α)

@[implicit_reducible]

instance Control.Monad.Trans.Resource.instMonadResourceT {m : Type → Type} [Monad m] : Monad (ResourceT m)

Equations

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

@[implicit_reducible]

instance Control.Monad.Trans.Resource.instMonadLiftIOResourceT {m : Type → Type} [MonadLift IO m] : MonadLift IO (ResourceT m)

Equations

• Control.Monad.Trans.Resource.instMonadLiftIOResourceT = { monadLift := fun {α : Type} (io : IO α) (x : IO.Ref Control.Monad.Trans.Resource.CleanupMap✝) => MonadLift.monadLift io }

def Control.Monad.Trans.Resource.allocate {α : Type} (acquire : IO α) (release : α → IO Unit) : ResourceT IO (ReleaseKey × α)

Register a resource with its cleanup action. Returns a ReleaseKey that can be used to release early.

Equations

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

def Control.Monad.Trans.Resource.release (key : ReleaseKey) : ResourceT IO Unit

Release a resource early. No-op if already released.

Equations

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

def Control.Monad.Trans.Resource.runResourceT {α : Type} (action : ResourceT IO α) : IO α

Run a ResourceT computation. All registered cleanup actions execute on completion in LIFO order, even on exceptions.

Equations

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

theorem Control.Monad.Trans.Resource.releaseKey_eq (a b : ReleaseKey) : a = b ↔ a.id = b.id

ReleaseKey equality is by id.