pub fn glb_perms<'db>(
env: &Env<'db>,
perm1: RedPerm<'db>,
perm2: RedPerm<'db>,
) -> Option<RedPerm<'db>>Expand description
The greatest lower bound (GLB) of two permissions (perm1, perm2), if it exists.
The GLB perm3 is a permission such that perm3 <: perm1 and perm3 <: perm2
but also there is no other mutual lower bound perm4 where perm3 <: perm4.
In other words, if perm1 and perm2 represent upper bounds in inference
(i.e., for some inference variable ?X, ?X <: perm1 and ?X <: perm2),
then perm3 combines those two bounds on ?X into a single bound ?X <: perm3
that must also hold (because there is no possible value for ?X that wouldn’t
satisfy it).
§Examples
glb_perms([our], [ref[x]]) = [our]glb_perms([ref[x] mut[y.z]], [ref[x.y] mut[y]]) = [ref[x.y] mut[y.z]]