def add_eq0

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64light.bend:71

import Base

71def add_eq0(+a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:
72  match a:
73    case 0n:
74      {==}
75    case 1n+ +ap:
76      {==}