Method mvar

crates/common/src/env.rs:442–447

Constructs a universe-level metavariable with the given name.

(x: Name)

    }
  }
  /// Constructs `imax x y` (impredicative max).
  pub fn imax(x: Level, y: Level) -> Self {
    let mut hasher = blake3::Hasher::new();
    hasher.update(&[UIMAX]);
    hasher.update(x.get_hash().as_bytes());
    hasher.update(y.get_hash().as_bytes());
    Level(Arc::new(LevelData::Imax(x, y, hasher.finalize())))
  }
  /// Constructs a universe parameter with the given name.