def add_swap

bendtorch-core@0.1.0.0 · src/shape/nat_proofs.bend:44

import Base
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast

44def add_swap(+a: Nat, +b: Nat, -c: Nat) -> {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}:
45  match a:
46    case 0n:
47      {==}
48    case 1n+p:
49      %Equal.sym(Nat, Nat.add(p, Nat.add(b, c)), Nat.add(b, Nat.add(p, c)), add_swap(p, b, c)) : {1n+_ == Nat.add(b, 1n+Nat.add(p, c)) : Nat}
50      Broadcast.add_succ(b, Nat.add(p, c))