Method cnst

crates/common/src/env.rs:860–868

Constructs a constant reference with universe level arguments.

(x: Name, us: Vec<Level>)

  /// Constructs a metavariable expression.
  pub fn mvar(x: Name) -> Self {
    let mut hasher = blake3::Hasher::new();
    hasher.update(&[EMVAR]);
    hasher.update(x.get_hash().as_bytes());
    Expr(Arc::new(ExprData::Mvar(x, hasher.finalize())))
  }

  /// Constructs a sort expression from a universe level.
  pub fn sort(x: Level) -> Self {
    let mut hasher = blake3::Hasher::new();
    hasher.update(&[ESORT]);
    hasher.update(x.get_hash().as_bytes());