def lt_succ

bend-ml-bpe-tokenizer@0.1.3.0 · main.bend:561

import Base

561# n < 1 + n
562def lt_succ(n: Nat) -> {True{} == Nat.is_lt(n, 1n+n) : Bool}:
563  match n:
564    case 0n:
565      {==}
566    case 1n+p:
567      lt_succ(p)