def add_zero

bendtorch-core@0.1.0.0 · src/shape/broadcast_proofs.bend:156

import Base

156def add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
157  match a:
158    case 0n:
159      {==}
160    case 1n+p:
161      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
162      {==}