def covered

stelliferous@0.0.2.0 · traversal_lanes.bend:91

import Base

91# An array of 2^depth values holds the count positions from position, within
92# the depths the refinement proof covers.
93def covered(+depth: Nat,+position: U32,+count: Nat) -> Bool:
94  Nat.is_le(depth,30n) && Nat.is_le(Nat.add(U32.to_nat(position),count),U32.to_nat(U32.shln(1,depth)))