Method try_def_eq_unit

crates/kernel/src/def_eq.rs:856–897

Unit-like type: non-recursive, 0 indices, 1 ctor with 0 fields. If both values inhabit the same unit-like type, they're def-eq.

(
    &mut self,
    a: &KExpr<M>,
    b: &KExpr<M>,
  )

  /// Returns true iff `ty` is a propositional type — i.e. its sort is
  /// `Sort 0`. Memoized on `(ty.hash_key(), ctx_hash)` because the answer
  /// is a pure function of the type and the relevant context suffix.
  ///
  /// On a hit this is one `FxHashMap` probe; on a miss it pays the
  /// existing `infer ∘ whnf` chain and stores the result. Errors from
  /// the inner chain are propagated as `Ok(false)` (treating ill-typed
  /// metadata as non-prop), matching the previous behaviour of
  /// `try_proof_irrel`.
  pub(crate) fn is_prop_type(&mut self, ty: &KExpr<M>) -> bool {
    let cache_key = (ty.hash_key(), self.ctx_addr_for_lbr(ty.lbr()));
    if let Some(&cached) = self.env.is_prop_cache.get(&cache_key) {
      self.env.perf.record_is_prop_hit();
      return cached;
    }
    self.env.perf.record_is_prop_miss();
    self.record_hot_miss("is-prop", ty);

    // infer(ty) returns the Sort that classifies `ty`. WHNF is needed because
    // the inferred sort may be wrapped in `mdata` or a let-bound sort
    // synonym before being structurally `Sort u`.
    let result = match self.with_infer_only(|tc| tc.infer(ty)) {
      Ok(sort) => match self.whnf(&sort) {
        Ok(reduced) => match reduced.data() {
          ExprData::Sort(u, _) => u.is_zero(),
          _ => false,
        },
        Err(_) => false,
      },
      Err(_) => false,
    };
    self.env.is_prop_cache.insert(cache_key, result);
    result
  }

  /// Unit-like type: non-recursive, 0 indices, 1 ctor with 0 fields.
  /// If both values inhabit the same unit-like type, they're def-eq.
  fn try_def_eq_unit(
    &mut self,
    a: &KExpr<M>,
    b: &KExpr<M>,
  ) -> Result<bool, TcError<M>> {
    let a_ty = match self.with_infer_only(|tc| tc.infer(a)) {
      Ok(ty) => ty,
      Err(_) => return Ok(false),
    };
    let a_ty_w = match self.whnf(&a_ty) {