def nat_eq_refl

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

import bend-ml-bpe-tokenizer@0.1.3.0/main.bend as BendMlBpeTokenizer

import Base

281def nat_eq_refl(a: Nat) -> {True{} == Nat.is_eq(a, a) : Bool}:
282  match a:
283    case 0n:
284      {==}
285    case 1n+p:
286      nat_eq_refl(p)

Uses (3)

Used by (2)