def Nat.read.trim

Base · base.bend:2317

2317# 2^48-1 is the text 281474976710655. Past leading zeros, fewer than
2318# fifteen characters fit, more do not, and fifteen compare as text;
2319# Nat.read.go still refuses a non-digit. The gate is a def, not a
2320# Bool.pick: an argument is built before the call, and reading a string
2321# that does not fit would build a Nat past the bound. A law that reads
2322# "7" never builds the unary nat (each digit once divided it).
2323def Nat.read.trim(s: String) -> String:
2324  match s:
2325    case SCon{'0', t}:
2326      Nat.read.trim(t)
2327    case t:
2328      t