law at_val

lawful-bytes@0.1.1.0 · proof_core.bend:57

import Base
import lawful-words@0.1.0.0/defs.bend as W
import lawful-arrays@0.1.0.0/proof_tree.bend as P

57law at_val:
58  for +len: U32
59  for +t: P.Tree<U32>
60  for +i: U32
61  {AT(len, t, i) == W.byte(WD(t, (i >> 2n : U32)), U32.to_nat((i .&. 3 : U32))) : U32}