Skip to main content

permission_split_ty

oxilean_std::program_logics::functions

Function permission_split_ty 

Source 
pub fn permission_split_ty() -> Expr
Expand description

PermissionSplit: p = p1 + p2 justifies l↦{p}v ⊢ l↦{p1}v ∗ l↦{p2}v. Type: Prop