def succ_not_zero

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:468

import bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend as SignedPROOF

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

468def succ_not_zero(-x: Nat, equal: {1n+x == 0n : Nat}) -> Empty:
469  Arith.clash(Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n), 1n+x, 0n, equal))

Uses (6)

Used by (2)