def cursor_inside
bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:553
import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
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
553def cursor_inside(+shape: Shape.Shape, +cursor: Nat, +index: U32,
554 converted: {U32.to_nat(index) == cursor : Nat}, below: Shape.LT(cursor, Shape.elements(shape))) ->
555 {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
556 Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))),
557 Nat.is_lt(cursor, Shape.logical_numel(Shape.dimensions(shape))), True{},
558 Equal.cong(Nat, Bool, n => Nat.is_lt(n, Shape.logical_numel(Shape.dimensions(shape))), U32.to_nat(index), cursor, converted),
559 Equal.trans(Bool, Nat.is_lt(cursor, Shape.logical_numel(Shape.dimensions(shape))), Nat.is_lt(cursor, Shape.elements(shape)), True{},
560 Equal.cong(Nat, Bool, n => Nat.is_lt(cursor, n), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements(shape),
561 Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape))),
562 Equal.sym(Bool, True{}, Nat.is_lt(cursor, Shape.elements(shape)), Nats.lt_true(cursor, Shape.elements(shape), below))))