Method param

crates/common/src/env.rs:435–440

Constructs a universe parameter with the given name.

(x: Name)

  /// `Some((Zero, n))`. Otherwise returns `None`.
  pub fn explicit_offset(&self) -> Option<(Level, u64)> {
    let (base, n) = self.peel_succ();
    if matches!(base.as_data(), LevelData::Zero(_)) {
      Some((base, n))
    } else {
      None
    }
  }
  /// Constructs `imax x y` (impredicative max).
  pub fn imax(x: Level, y: Level) -> Self {