~/jendhub

def AP.get_v_new

bend-osdev-array@0.1.0.1 · PROOF.bend:1165

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base

1165def AP.get_v_new(-T: Data, +d: Nat, +v: T, n: U32, +i: U32, z: Bool) -> {AP.get_v(T, AP.tnew(T, d, v), n, i, z) == v : T}:
1166  match d z:
1167    case 0n _:
1168      {==}
1169    case 1n+p True{}:
1170      +h = U32.shr(n)
1171      AP.get_v_new(T, p, v, h, i, U32.is_lt(i, U32.shr(h)))
1172    case 1n+p False{}:
1173      +h = U32.shr(n)
1174      +j = U32.sub(i, h)
1175      AP.get_v_new(T, p, v, h, j, U32.is_lt(j, U32.shr(h)))

Uses (8)

Used by (1)