printSorriesStx — Mathlib

Lean4
/-- - `#print sorries` prints all sorries that the current module depends on.
- `#print sorries id1 id2 ... idn` prints all sorries that the provided declarations depend on.
- `#print sorries in CMD` prints all the sorries in declarations added by the command.

Displayed sorries are hoverable and support "go to definition".
-/
@[command_parser 1000]
public meta def printSorriesStx : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.PrintSorries.printSorriesStx 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#print ")
        ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "sorries" false✝))
      (ParserDescr.unary✝ `many
        (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `ident))))
Похожие утверждения