def Nat.check_eq

bendtorch@1.3.0.0 · tensor.bend:109

import Base

109# a proof that a == b, when it holds (reshape's count, read at run time)
110def Nat.check_eq(a: Nat, b: Nat) -> Maybe<&1, {a == b : Nat}>:
111  match a b:
112    case 0n 0n:
113      Some{{==}}
114    case 1n+p 1n+q:
115      nat_eq_succ(p, q, Nat.check_eq(p, q))
116    case _ _:
117      None{}