Struct chalk_ir::UniverseMap

pub struct UniverseMap {
    pub universes: Vec<UniverseIndex>,
}

Maps the universes found in the u_canonicalize result (the “canonical” universes) to the universes found in the original value (and vice versa). When used as a folder – i.e., from outside this module – converts from “canonical” universes to the original (but see the UMapToCanonical folder).

Fields

universes: Vec<UniverseIndex>

A reverse map – for each universe Ux that appears in quantified, the corresponding universe in the original was universes[x].

Implementations

impl UniverseMap

pub fn new() -> Self

Creates a new universe map.

pub fn num_canonical_universes(&self) -> usize

Number of canonical universes.

Trait Implementations

impl Clone for UniverseMap

fn clone(&self) -> UniverseMap

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for UniverseMap

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

Formats the value using the given formatter.