Struct LevelArena 

pub struct LevelArena { /* private fields */ }

Arena for interning universe levels

Implementations

impl LevelArena

pub fn new() -> Self

Create a new level arena

pub fn intern(&mut self, level: Level) -> LevelId

Intern a level and return its ID

pub fn get(&self, id: LevelId) -> Option<&Level>

Get a level by its ID

pub fn zero(&mut self) -> LevelId

Get the zero level ID

pub fn constant(&mut self, n: u32) -> LevelId

Create a concrete level

pub fn param(&mut self, n: u32) -> LevelId

Create a parameter level

pub fn succ(&mut self, id: LevelId) -> LevelId

Create a successor level

pub fn max(&mut self, a: LevelId, b: LevelId) -> LevelId

Create a max level

pub fn imax(&mut self, a: LevelId, b: LevelId) -> LevelId

Create an imax level

pub fn normalize(&mut self, id: LevelId) -> LevelId

Normalize a level (reduce max/imax where possible)

Trait Implementations

impl Default for LevelArena

fn default() -> Self

Returns the “default value” for a type.