~/jendhub

def holds_false

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

import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

433def holds_false(+dimensions: List<&2, U32>, +nonempty: {Nat.is_lt(0n, Shape.logical_numel(dimensions)) == True{} : Bool},
434  decision: Shape.BoolCase<Slice.holds_zero(dimensions)>) -> {Slice.holds_zero(dimensions) == False{} : Bool}:
435  match decision:
436    case Shape.BFalse{equal}:
437      Equal.sym(Bool, False{}, Slice.holds_zero(dimensions), equal)
438    case Shape.BTrue{equal}:
439      Empty.absurd({Slice.holds_zero(dimensions) == False{} : Bool},
440        Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(0n, Shape.logical_numel(dimensions)), True{},
441          Equal.cong(Nat, Bool, v => Nat.is_lt(0n, v), 0n, Shape.logical_numel(dimensions),
442            Equal.sym(Nat, Shape.logical_numel(dimensions), 0n, zero_numel(dimensions, Equal.sym(Bool, True{}, Slice.holds_zero(dimensions), equal)))),
443          nonempty)))

Uses (14)

Used by (1)