def checked_index_allowed

bendtorch-core@0.1.0.0 · src/tensor/lifecycle.bend:307

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

307def checked_index_allowed(+depth: Nat, +length: Nat, +index: U32,
308  +checked: {Storage.index_matches(depth, length, index) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}:
309  %natural_equal(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
310    Equal.sym(Bool, Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)), True{},
311      and_left_true(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
312        Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked))) :
313    {Nat.is_lt(_, length) == True{} : Bool}
314  and_right_true(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
315    Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked)