def succ_zero

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

import Base

37def succ_zero(-value: Nat, equal: {1n+value == 0n : Nat}) -> Empty:
38  %equal : positive(_)
39  Unit{}