pub open spec fn incl<RA: ResourceAlgebra>(a: RA, b: RA) -> boolExpand description
{ exists |c| RA::op(a, c) == b }The preorder relation.
incl(a, b) (or a ≼ b) means that there is some c such that a · c == b
pub open spec fn incl<RA: ResourceAlgebra>(a: RA, b: RA) -> bool{ exists |c| RA::op(a, c) == b }The preorder relation.
incl(a, b) (or a ≼ b) means that there is some c such that a · c == b