def is_eq_refl

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:234

import Base

234def is_eq_refl(+a: Nat) -> {Nat.is_eq(a, a) == True{} : Bool}:
235  match a:
236    case 0n:
237      {==}
238    case 1n+p:
239      is_eq_refl(p)