def flat_view
bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:125
import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
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
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
125def flat_view(-shape: Shape.Shape, +index: Nat, +verdict: Shape.BoolCase<Nat.is_lt(index, Shape.elements(shape))>, fits: {True{} == Nat.is_lt(index, Shape.elements(shape)) : Bool}) -> {Laws.index_result(shape, Shape.flat_checked.finish(shape, index, verdict)) == Some{U32.from_nat(index)} : Maybe<&2, U32>}:
126 match verdict:
127 case Shape.BFalse{equal}:
128 Empty.absurd({Laws.index_result(shape, Shape.flat_checked.finish(shape, index, Shape.BFalse{equal})) == Some{U32.from_nat(index)} : Maybe<&2, U32>}, Nats.contradiction(Nat.is_lt(index, Shape.elements(shape)), fits, equal))
129 case Shape.BTrue{equal}:
130 {==}