Array.write_path: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/storage/array.bend as Array Lines 61-75 of bendtorch-core@0.1.0.0/src/storage/array.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&start_line=61&end_line=75 import Base import bendtorch-core@0.1.0.0/src/storage/model.bend as Model def write_path(-T: Data, d: Nat, array: Array, path: Model.Path(d), value: T) -> Array: match d array: case 0n ALeaf{old}: ALeaf{value} case 0n ANode{xs, ys}: ANode{xs, ys} case 1n+p ALeaf{old}: ALeaf{old} case 1n+p ANode{xs, ys}: Model.Step{bit, rest} = path match bit: case False{}: ANode{write_path(T, p, xs, rest, value), ys} case True{}: ANode{xs, write_path(T, p, ys, rest, value)} Uses (5): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Path https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Step