Method ensure_sort

crates/kernel/src/tc.rs:643–653

WHNF, then ensure it's a Sort. Returns the universe level.

(&mut self, e: &KExpr<M>)

  }

  // -----------------------------------------------------------------------
  // Universe helpers
  // -----------------------------------------------------------------------

  /// WHNF, then ensure it's a Sort. Returns the universe level.
  pub fn ensure_sort(&mut self, e: &KExpr<M>) -> Result<KUniv<M>, TcError<M>> {
    // Fast path: already a Sort, skip WHNF + tick.
    if let ExprData::Sort(u, _) = e.data() {
      return Ok(u.clone());
    }
    let w = self.whnf(e)?;
    match w.data() {
      ExprData::Sort(u, _) => Ok(u.clone()),
      _ => Err(TcError::TypeExpected),