Method lbr

crates/kernel/src/expr.rs:122–124

(&self)

  /// re-abstracted into de Bruijn binders before the result escapes the
  /// open scope. The flag lets callers (substitution, `abstract_fvars`,
  /// soundness assertions) skip walks when no fvars are reachable.
  pub has_fvars: bool,
  /// Lean mdata annotations. Semantically transparent, erased in Anon mode.
  pub mdata: M::MField<Vec<MData>>,
  /// Original level-spelling decoration (Meta-mode `Sort`/`Const` only;
  /// `None` everywhere else and when the stored spelling is already