Spec.passes: def of bendtorch@1.3.0.0 Import: import bendtorch@1.3.0.0/spec.bend as Spec Lines 193-200 of bendtorch@1.3.0.0/spec.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/spec.bend&start_line=193&end_line=200 import Base # r passes of tree_sum; tree_sum (ts_go) stops once one cell is left, and a pass leaves one cell as it is, so the sum of # m cells is passes(r, row) for any r at least the number of passes it makes def passes(r: Nat, xs: List<&2, Sum>) -> List<&2, Sum>: match r: case 0n: xs case 1n+q: spass(passes(q, xs)) Uses (4): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=Sum https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=spass