pub struct Levels { /* private fields */ }Implementations§
Source§impl Levels
impl Levels
pub fn new() -> Levels
pub fn intern(&mut self, node: LevelNode) -> LevelId
pub fn len(&self) -> usize
pub fn is_empty(&self) -> bool
pub fn node(&self, l: LevelId) -> LevelNode
pub fn has_param(&self, l: LevelId) -> bool
pub fn list(&mut self, ls: &[LevelId]) -> LevelsId
pub fn get_list(&self, id: LevelsId) -> &[LevelId]
pub fn succ(&mut self, l: LevelId) -> LevelId
Sourcepub fn sprop(&mut self) -> LevelId
pub fn sprop(&mut self) -> LevelId
LOGOS’s SProp (see LevelNode::SProp).
pub fn is_sprop(&self, l: LevelId) -> bool
pub fn param(&mut self, n: NameId) -> LevelId
pub fn max_raw(&mut self, a: LevelId, b: LevelId) -> LevelId
pub fn imax_raw(&mut self, a: LevelId, b: LevelId) -> LevelId
pub fn of_nat(&mut self, n: u64) -> LevelId
Sourcepub fn is_never_zero(&self, l: LevelId) -> bool
pub fn is_never_zero(&self, l: LevelId) -> bool
Syntactic: true only when l is nonzero under every assignment (is_never_zero).
Sourcepub fn max(&mut self, a: LevelId, b: LevelId) -> LevelId
pub fn max(&mut self, a: LevelId, b: LevelId) -> LevelId
Lean’s mkLevelMax': max with the cheap simplifications the kernel applies.
Sourcepub fn instantiate(
&mut self,
l: LevelId,
ps: &[NameId],
us: &[LevelId],
) -> LevelId
pub fn instantiate( &mut self, l: LevelId, ps: &[NameId], us: &[LevelId], ) -> LevelId
Replaces each Param(ps[i]) by us[i].
Sourcepub fn substitution(&mut self, ps: &[NameId], us: LevelsId) -> SubstId
pub fn substitution(&mut self, ps: &[NameId], us: LevelsId) -> SubstId
The substitution of the levels us for the parameters ps (pairwise; a parameter without
a level is left as it is). Replacing each parameter by itself is the identity.
Sourcepub fn subst(&mut self, l: LevelId, s: SubstId) -> LevelId
pub fn subst(&mut self, l: LevelId, s: SubstId) -> LevelId
l under the substitution s — exactly Levels::instantiate with its parameters and
levels, remembered.
Sourcepub fn subst_list(&mut self, ls: LevelsId, s: SubstId) -> LevelsId
pub fn subst_list(&mut self, ls: LevelsId, s: SubstId) -> LevelsId
Every level of ls under the substitution s.
Sourcepub fn mentions_sprop(&self, l: LevelId) -> bool
pub fn mentions_sprop(&self, l: LevelId) -> bool
Whether SProp occurs anywhere in l.
Sourcepub fn mentions_param(&self, l: LevelId, p: NameId) -> bool
pub fn mentions_param(&self, l: LevelId, p: NameId) -> bool
Whether l mentions the parameter p.
Sourcepub fn undef_param(&self, l: LevelId, ps: &[NameId]) -> Option<NameId>
pub fn undef_param(&self, l: LevelId, ps: &[NameId]) -> Option<NameId>
The first parameter of l not listed in ps.
Sourcepub fn leq(&mut self, u: LevelId, v: LevelId) -> bool
pub fn leq(&mut self, u: LevelId, v: LevelId) -> bool
u ≤ v under every assignment of the parameters.
pub fn equiv(&mut self, u: LevelId, v: LevelId) -> bool
pub fn equiv_lists(&mut self, a: LevelsId, b: LevelsId) -> bool
Sourcepub fn is_always_zero(&self, l: LevelId) -> bool
pub fn is_always_zero(&self, l: LevelId) -> bool
l is zero under every assignment of its parameters. Exact, and structural: a successor
never is, a parameter may be one, max a b is exactly when both are, imax a b exactly
when b is (it is 0 when b is and at least b otherwise).