Method get_level_params

crates/common/src/env.rs:1437–1448

Returns the universe level parameter names of this constant.

(&self)

      ConstantInfo::QuotInfo(v) => &v.cnst.typ,
      ConstantInfo::InductInfo(v) => &v.cnst.typ,
      ConstantInfo::CtorInfo(v) => &v.cnst.typ,
      ConstantInfo::RecInfo(v) => &v.cnst.typ,
    }
  }

  /// Returns the value of this constant, if it has one (definitions, theorems, opaques).
  pub fn get_value(&self) -> Option<&Expr> {
    match self {
      ConstantInfo::DefnInfo(v) => Some(&v.value),
      ConstantInfo::ThmInfo(v) => Some(&v.value),
      ConstantInfo::OpaqueInfo(v) => Some(&v.value),
      _ => None,
    }
  }