~/jendhub

def sum_zero

bendtorch-core@0.1.0.0 · src/shape/unique_proofs.bend:41

import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as UniqueProofs
import Base

41def sum_zero(+a: Nat, -b: Nat, equal: {Nat.add(a, b) == 0n : Nat}) -> {a == 0n : Nat}:
42  match a:
43    case 0n:
44      {==}
45    case 1n+p:
46      Empty.absurd({1n+p == 0n : Nat}, succ_zero(Nat.add(p, b), equal))

Uses (4)

Used by (1)