Method def_eq_ctx_key

crates/kernel/src/tc.rs:381–383

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

  ///
  /// Def-eq may inspect both sides through WHNF, inference, proof
  /// irrelevance, eta, and structural recursion. All of those operations are
  /// bounded by the loose-bound-variable range reachable from the compared
  /// expressions, so the relevant context is the suffix needed by the larger
  /// `lbr`.
  #[inline]
  pub fn def_eq_ctx_key(&mut self, a: &KExpr<M>, b: &KExpr<M>) -> CtxAddr {