Equations
- Lean.Elab.Command.elabPrint x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.print = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; cond (Lean.Syntax.isOfKind discr_2 `ident) (let id := discr_2; let tk := discr_1; Lean.withRef tk (Lean.Elab.Command.printId id)) (let discr_3 := Lean.Syntax.getArg discr 1; cond (Lean.Syntax.isOfKind discr_3 `strLit) (let s := discr_3; let tk := discr_1; Lean.Elab.logInfoAt tk (Function.comp Lean.MessageData.ofFormat Lean.format (Option.get! (Lean.Syntax.isStrLit? s)))) (let discr := Lean.Syntax.getArg discr 1; Lean.throwError (Lean.toMessageData "invalid #print command"))) else let discr := x; Lean.throwError (Lean.toMessageData "invalid #print command")
- visited : Lean.NameSet
- axioms : Array Lean.Name
@[inline]
Equations
- Lean.Elab.Command.elabPrintAxioms x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.printAxioms = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr 2; let id := discr; let tk := discr_1; Lean.withRef tk do let cs ← Lean.Elab.resolveGlobalConstWithInfos id List.forM cs Lean.Elab.Command.printAxiomsOf else let discr := x; Lean.Elab.throwUnsupportedSyntax