TraceContext.Budget.take: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
Lines 2017-2026 of bend-trace-context@0.2.0.0/trace_context.bend: https://jend.leeeet.dev/read.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&start_line=2017&end_line=2026

import Base

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

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat