def cursor_bounds

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:732

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

732def cursor_bounds(+fuel: Nat, +cursor: Nat, +limit: Nat,
733  bound: Shape.LE(Nat.add(1n+fuel, cursor), limit)) -> {Nat.is_lt(cursor, limit) == True{} : Bool}:
734  Conversion.le_successor_lt(cursor, limit,
735    Equal.sym(Bool, True{}, Nat.is_le(1n+cursor, limit),
736      Nats.le_true(1n+cursor, limit,
737        Nats.le_add_left(1n+cursor, fuel, limit,
738          %add_comm(fuel, cursor) : Shape.LE(1n+_, limit)
739          bound))))