def inside_at

bendtorch-core@0.1.0.0 · src/tensor/contracts/pointwise_proof.bend:124

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise

124def inside_at(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +count: Nat, +bound: Nat,
125  all: {Pointwise.inside(~P, ~map, plan, count, bound) == True{} : Bool}, +index: Nat,
126  below: {Nat.is_lt(index, count) == True{} : Bool}) -> {Nat.is_lt(map(plan, index), bound) == True{} : Bool}:
127  match count:
128    case 0n:
129      Empty.absurd({Nat.is_lt(map(plan, index), bound) == True{} : Bool}, Arith.lt_zero(index, below))
130    case 1n+previous:
131      inside_split(~P, ~map, plan, previous, bound, all, index, below,
132        earlier => before => inside_at(~P, ~map, plan, previous, bound, earlier, index, before),
133        Shape.bool_case(Nat.is_eq(index, previous)))