def bound_within

bendtorch-core@0.1.0.0 · src/shape/construct_proofs.bend:13

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

13def bound_within(-dims: List<&2, Nat>, -size: Nat, -exact: {size == Shape.numel(dims) : Nat}, +decision: Shape.BoolCase<Nat.is_le(size, 1048576n)>, fits: {True{} == Nat.is_le(size, 1048576n) : Bool}) -> {True{} == within(dims, Shape.capacity.bound(dims, size, exact, decision)) : Bool}:
14  match decision:
15    case Shape.BFalse{equal}:
16      Empty.absurd({True{} == False{} : Bool}, Nats.contradiction(Nat.is_le(size, 1048576n), fits, equal))
17    case Shape.BTrue{equal}:
18      {==}