Struct Level 

pub struct Level(/* private fields */);

A universe level.

Levels form expressions over zero, successor, max, imax, parameters, and metavariables.

Structural sharing (wave5 Stage F): Level is a newtype over a reference-counted cell holding its outermost node (LevelKind), so cloning a whole level — e.g. every element of the Vec<Level> a Const carries — is an O(1) refcount bump, and sub-levels are shared by pointer. Match on the outermost node through Level::view.

Each level also stores a hash of its own structure, computed when it is built from the stored hashes of its sub-levels (see the kernel-private structural_hash module) — so an Expr that carries levels (a Sort, a Const) folds them into its own hash in O(1) each, without walking them.

Equality is exactly structural: the same allocation is equal, different stored hashes are different (equal levels always hash equal), and otherwise the nodes are compared. Hash writes the structure as it always did (not the stored hash), so a HashMap<Level, _> behaves as before.

Implementations

impl Level

pub fn view(&self) -> LevelView<'_>

Borrow this level’s outermost node for matching. O(1).

pub fn zero() -> Self

Create Zero level.

pub fn succ(l: Level) -> Self

Create a successor level.

pub fn max(l1: Level, l2: Level) -> Self

Create a max level.

pub fn imax(l1: Level, l2: Level) -> Self

Create an imax level.

pub fn param(name: Name) -> Self

Create a parameter level.

pub fn mvar(id: LevelMVarId) -> Self

Create a level metavariable.

pub fn is_zero(&self) -> bool

Check if this is Zero.

pub fn is_param(&self) -> bool

Check if this is a parameter.

pub fn is_mvar(&self) -> bool

Check if this is a metavariable.

pub fn is_succ(&self) -> bool

Check if this is a successor.

pub fn is_max(&self) -> bool

Check if this is a max.

pub fn is_imax(&self) -> bool

Check if this is an imax.

pub fn is_not_zero(&self) -> bool

Check if this level is definitely not zero.

Returns true if we can statically determine this is >= 1.

pub fn has_mvar(&self) -> bool

Check if this level contains any metavariables.

pub fn has_param(&self) -> bool

Check if this level contains any parameters.

pub fn depth(&self) -> usize

Get the depth (nesting) of this level expression.

pub fn from_nat(n: u32) -> Self

Create a numeric level succ^n(zero).

pub fn to_nat(&self) -> Option<u32>

Try to convert to a numeric level.

Returns Some(n) if this is succ^n(zero), None otherwise.

Trait Implementations

impl Clone for Level

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Level

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats as Level(<kind>) — the output of the derived implementation when Level wrapped the node kind directly. Code that hashes or orders terms by their Debug text depends on this spelling.

impl Display for Level

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Level

impl Hash for Level

fn hash<H: Hasher>(&self, state: &mut H)

Writes the structure, exactly as the derived implementation did when Level wrapped the node kind directly.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Level

fn eq(&self, other: &Level) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.