def add_succ

bendtorch-core@0.1.0.0 · src/storage/arith.bend:29

import Base

29def add_succ(a: Nat, -b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
30  match a:
31    case 0n:
32      {==}
33    case 1n+p:
34      %add_succ(p, b) : {1n+Nat.add(p, 1n+b) == 1n+_ : Nat}
35      {==}