Function nat_align_down Copy item path

pub open spec fn nat_align_down(x: nat, align: nat) -> nat

align > 0,

{ (x - x % align) as nat }