Skip to main content

perm_u64_with_value

ostd::specs::mm::frame::meta_owners

Function perm_u64_with_value 

Source 
pub proof fn perm_u64_with_value(p: PermissionU64, v: u64)
Expand description
ensures
perm_u64_with(p, v).value() == v,
perm_u64_with(p, v).id() == p.id(),