def lab_take

bend-ml-tensor-fork@0.1.6.0 · main.bend:392

import Base

392# up to n labels into a, counted in k; the rest stays a list
393def lab_take(n: Nat, labels: List<&2, Nat>, +mm1: Nat, +c: Nat, +i: U32, +k: Nat, a: Array<U32>) -> CL:
394  match n labels:
395    case 0n ls:
396      CL{a, k, ls}
397    case 1n+p Nil{}:
398      CL{a, k, Nil{}}
399    case 1n+p Con{+y, t}:
400      lab_take(p, t, mm1, c, (i + 1 : U32), 1n+k, Array.set(U32, a, i, U32.from_nat(lab_fit(Nat.is_le(y, mm1), y, c))))