def AP.val_shln

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

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

449def AP.val_shln(+d: Nat, h: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.shln(1, d)) == A.Arrays.slots(d) : Nat}:
450  %AP.pw_shln(d) : {U32.to_nat(_) == A.Arrays.slots(d) : Nat}
451  AP.val_pw(32n, d, h)