def trace

bendtorch-core@0.1.0.0 · src/storage/refinement.bend:6

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

6def trace(d: Nat, +n: U32, +i: U32, z: Bool) -> Model.Path(d):
7  match d z:
8    case 0n _:
9      Unit{}
10    case 1n+p True{}:
11      Model.Step{False{}, trace(p, U32.shr(n), i,
12        U32.is_lt(i, U32.shr(U32.shr(n))))}
13    case 1n+p False{}:
14      +j = U32.sub(i, U32.shr(n))
15      Model.Step{True{}, trace(p, U32.shr(n), j,
16        U32.is_lt(j, U32.shr(U32.shr(n))))}