def right_inside

bendtorch-core@0.1.0.0 · src/tensor/contracts/dot_proof.bend:106

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/tensor/contracts/pointwise.bend as Pointwise
import bendtorch-core@0.1.0.0/src/tensor/contracts/dot.bend as Dot

106def right_inside(+inner: Nat, +columns: Nat, +row: Nat, +column: Nat,
107  +column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right: Shape.Shape,
108  +right_extents: {Shape.extents(right) == [inner, columns] : List<&2, Nat>}, +count: Nat,
109  +room: {Nat.is_le(count, inner) == True{} : Bool}) ->
110  {Pointwise.inside(~Dot.Cell, ~Dot.right_index, Dot.Cell{row, column, inner, columns}, count, Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool}:
111  match count:
112    case 0n:
113      {==}
114    case 1n+previous:
115      +cell : Dot.Cell = Dot.Cell{row, column, inner, columns}
116      +bound = Shape.logical_numel(Shape.dimensions(right))
117      %Equal.sym(Bool, Pointwise.inside(~Dot.Cell, ~Dot.right_index, cell, previous, bound), True{},
118        right_inside(inner, columns, row, column, column_below, right, right_extents, previous,
119          Conversion.le_predecessor(previous, inner, room))) :
120        {Bool.and(_, Nat.is_lt(Dot.right_index(cell, previous), bound)) == True{} : Bool}
121      %Equal.sym(Bool, Nat.is_lt(Dot.right_index(cell, previous), bound), True{},
122        right_below(inner, columns, row, column, column_below, right, right_extents, previous,
123          Conversion.le_successor_lt(previous, inner, room))) :
124        {Bool.and(True{}, _) == True{} : Bool}
125      {==}