~/jendhub

def zero_not_one

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

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

471def zero_not_one(equal: {0n == 1n : Nat}) -> Empty:
472  Arith.clash_true(Equal.cong(Nat, Bool, n => Nat.is_eq(n, 0n), 0n, 1n, equal))

Uses (6)

Used by (1)