law slot_small

lawful-arrays@0.1.0.0 · LAWS.bend:197

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

197law slot_small:
198  for i: U32
199  for d: Nat
200  for h: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
201  {D.slot(i, d) == U32.to_nat(i) : Nat}