structure Lean.Elab.Command.PrintPrefixConfig : Type

Options to control #print prefix command and getMatchingConstants.

• imported : Bool

  Include declarations in imported environment.

• propositions : Bool

  Include declarations whose types are propositions.

• propositionsOnly : Bool

  Exclude declarations whose types are not propositions.

• showTypes : Bool

  Print the type of a declaration.

• internals : Bool

  Include internal declarations (names starting with _, match_ or proof_)

def Lean.Elab.Command.elabPrintPrefixConfig : Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Command.PrintPrefixConfig

Function elaborating Config.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.printPrefix : Lean.ParserDescr

The command #print prefix foo will print all definitions that start with the namespace foo.

For example, the command below will print out definitions in the List namespace:

#print prefix List

#print prefix can be controlled by flags in PrintPrefixConfig. These provide options for filtering names and formatting. For example, #print prefix by default excludes internal names, but this can be controlled via config:

#print prefix (config:={internals:=true}) List

By default, #print prefix prints the type after each name. This can be controlled by setting showTypes to false:

#print prefix (config:={showTypes:=false}) List

The complete set of flags can be seen in the documentation for Lean.Elab.Command.PrintPrefixConfig.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.elabPrintPrefix : Lean.Elab.Command.CommandElab

Implementation for #print prefix

Equations

• One or more equations did not get rendered due to their size.