def nat_clash

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:118

import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF

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

118def nat_clash(+x: Nat, e: {1n+x == 0n : Nat}) -> Empty:
119  Arith.clash(Equal.cong(Nat, Bool, v => Nat.is_eq(v, 0n), 1n+x, 0n, e))

Uses (6)

Used by (4)