def add_zero_r

bend-ml-tensor-array@0.1.19.0 · main.bend:1524

import Base

1524# a + 0 == a
1525def add_zero_r(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
1526  match a:
1527    case 0n:
1528      {==}
1529    case 1n+p:
1530      %add_zero_r(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
1531      {==}