ink

structure Lean.Meta.FindOptions : Type

• stage1 : Bool
• checkPrivate : Bool

ink

def Lean.Meta.findCore (ϕ : Lean.ConstantInfo → Lean.MetaM Bool) (opts : optParam Lean.Meta.FindOptions { stage1 := true, checkPrivate := false }) : Lean.MetaM (Array Lean.ConstantInfo)

Equations

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

ink

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)

Equations

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

ink

def Lean.Meta.find (msg : String) (ϕ : Lean.ConstantInfo → Lean.MetaM Bool) (opts : optParam Lean.Meta.FindOptions { stage1 := true, checkPrivate := false }) : Lean.Elab.TermElabM String

Equations

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

ink

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

Equations

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

ink

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

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

Equations

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