Documentation

Std.Tactic.PrintPrefix

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_)

Instances For

    Function elaborating Config.

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

      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.
      Instances For

        Implementation for #print prefix

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