Method sort

crates/common/src/env.rs:852–857

Constructs a sort expression from a universe level.

(x: Level)

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

  /// Constructs a metavariable expression.
  pub fn mvar(x: Name) -> Self {