TraceContext.Utf8.left: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
Lines 2028-2038 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=2028&end_line=2038

import Base

# What is left of a budget after a text, or None once the text exceeds it.
# Measuring stops at the first character beyond the budget, and a None budget
# stays None.
def Utf8.left(text: String, budget: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
  match text budget:
    case _ None{}:
      None{}
    case SNil{} Some{left}:
      Some{left}
    case SCon{char, tail} Some{left}:
      Utf8.left(tail, Budget.take(Utf8.width(char), left))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Budget.take
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/trace_context.bend&name=Utf8.width