def AP.get_new.go

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

import Base

1234def AP.get_new.go(-T: Data, +d: Nat, +v: T, +i: U32) -> {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}:
1235  +t = AP.tnew(T, d, v)
1236  +n = AP.size(T, t)
1237  +j = AP.mask(n, i)
1238  %Equal.sym(Array<T>, Array.new(T, d, v), AP.build(T, t), AP.new_eq(T, d, v)) : {Pair.snd(Array<T>, T, Array.get(T, _, i)) == v : T}
1239  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), AP.get_top(T, t, i)), AP.get_top_eq(T, t, i)) : {Pair.snd(Array<T>, T, _) == v : T}
1240  AP.get_v_new(T, d, v, n, j, AP.z(n, j))