law leaf_len

bend-ml-tensor-array@0.1.19.0 · main.bend:1821

import Base

1821# a leaf's list: read_l reads mleft + 1 numbers onto acc. By induction on mleft: with 0 left it
1822# reads one number onto acc (1 + the length of acc, by the definitions); with 1 + p left it reads
1823# one and recurses, and len_step moves the 1 out of the sum.
1824law leaf_len:
1825  for -r: Nat
1826  for -c: Nat
1827  for w: Array<F32>
1828  for +mleft: Nat
1829  for +idx: U32
1830  for +acc: List<&2, F32>
1831  for rc: Array<F32> & F32
1832  {bl_len(r, c, bv_g2(r, c, w, read_l(mleft, idx, acc, rc))) == Nat.add(1n+mleft, List.length(&2, F32, acc)) : Nat}