letImplDetailStx — Mathlib

Lean4
/-- Mathlib extension to preserve old behavior of structure instances.
We need to be able to `let` some implementation details that are still local instances.
Normally implementation detail fvars are not local instances,
but we need them to be implementation details so that `simp` will see them as "reducible" fvars.
-/
@[term_parser 1000]
public meta def letImplDetailStx : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `letImplDetailStx 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "let_impl_detail ")
              (ParserDescr.parser✝ `Lean.Parser.Term.ident))
            (ParserDescr.symbol✝ " := "))
          (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ "; "))
      (ParserDescr.cat✝ `term 0))
Похожие утверждения