def flat_index_inside
bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:598
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
598def flat_index_inside(+shape: Shape.Shape, +index: Shape.FlatIndex<shape>) ->
599 {Nat.is_lt(U32.to_nat(Shape.index_value(shape, index)), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
600 Shape.FIndex{+value, +bound} = index
601 %Shape.elements_exact(shape) :
602 {Nat.is_lt(U32.to_nat(U32.from_nat(value)), _) == True{} : Bool}
603 %Equal.sym(Nat, U32.to_nat(U32.from_nat(value)), value,
604 TransformProof.cursor_word_exact(shape, value, Conversion.lt_le(value, Shape.elements(shape), Equal.sym(Bool, True{}, Nat.is_lt(value, Shape.elements(shape)), bound)))) :
605 {Nat.is_lt(_, Shape.elements(shape)) == True{} : Bool}
606 Equal.sym(Bool, True{}, Nat.is_lt(value, Shape.elements(shape)), bound)