~/jendhub

def Budget.take

bend-trace-context@0.2.0.0 · trace_context.bend:2017

import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
import Base

2017# What is left of a budget after taking `need` octets, or None when less
2018# remains.
2019def Budget.take(need: Nat, budget: Nat) -> Maybe<&2, Nat>:
2020  match need budget:
2021    case 0n _:
2022      Some{budget}
2023    case 1n+more 0n:
2024      None{}
2025    case 1n+more 1n+left:
2026      Budget.take(more, left)

Uses (2)

Used by (1)