def nat_eq_sound

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

import Base

267def nat_eq_sound(a: Nat, b: Nat, e: {True{} == Nat.is_eq(a, b) : Bool}) -> {a == b : Nat}:
268  match a b:
269    case 0n 0n:
270      {==}
271    case 0n 1n+q:
272      %e : BD(_, Unit, {0n == 1n+q : Nat})
273      Unit{}
274    case 1n+p 0n:
275      %e : BD(_, Unit, {1n+p == 0n : Nat})
276      Unit{}
277    case 1n+p 1n+q:
278      %nat_eq_sound(p, q, e) : {1n+p == 1n+_ : Nat}
279      {==}