def row_from

mlbend-report@0.1.0.0 · main.bend:70

import Base

70# The row of the class i, from the column j on: n cells, the cell of
71# every class from j to j+n-1, ascending. The counted form is the
72# public one, because the law walks it: the counter of the cells left
73# is the argument that shrinks.
74def row_from(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat, +i: Nat, n: Nat, +j: Nat) ->
75  List<&2, Nat>:
76  match n:
77    case 0n:
78      Nil{}
79    case 1n+rest:
80      Con{cell(ys, ps, i, j), row_from(ys, ps, k, i, rest, (1n + j : Nat))}