Documentation

Mathlib.Tactic.PrintPrefix

source
structure Lean.Meta.FindOptions :
Type
Instances For
    source
    def Lean.Meta.findCore (ϕ : Lean.ConstantInfo → Lean.MetaM Bool) (opts : optParam Lean.Meta.FindOptions { stage1 := true, checkPrivate := false }) :
    Lean.MetaM (Array Lean.ConstantInfo)
    Instances For
      source
      def Lean.Meta.findCore.check (ϕ : Lean.ConstantInfo → Lean.MetaM Bool) (opts : optParam Lean.Meta.FindOptions { stage1 := true, checkPrivate := false }) (matches_ : Array Lean.ConstantInfo) (name : Lean.Name) (cinfo : Lean.ConstantInfo) :
      Lean.MetaM (Array Lean.ConstantInfo)
      Instances For
        source
        def Lean.Meta.find (msg : String) (ϕ : Lean.ConstantInfo → Lean.MetaM Bool) (opts : optParam Lean.Meta.FindOptions { stage1 := true, checkPrivate := false }) :
        Lean.Elab.TermElabM String
        Instances For
          source
          def Lean.Elab.Command.printPrefix :
          Lean.ParserDescr
          Instances For
            source
            def Lean.Elab.Command.elabPrintPrefix :
            Lean.Elab.Command.CommandElab

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

            Instances For