def
Lean.Meta.findCore
(ϕ : Lean.ConstantInfo → Lean.MetaM Bool)
(opts : optParam Lean.Meta.FindOptions { stage1 := true, checkPrivate := false })
:
Instances For
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)
:
Instances For
def
Lean.Meta.find
(msg : String)
(ϕ : Lean.ConstantInfo → Lean.MetaM Bool)
(opts : optParam Lean.Meta.FindOptions { stage1 := true, checkPrivate := false })
:
Instances For
The command #print prefix foo
will print all definitions that start with
the namespace foo
.