def Lean.getMatchingConstants {m : Type → Type} [Monad m] [Lean.MonadEnv m] (p : Lean.ConstantInfo → m Bool) (includeImports : optParam Bool true) : m (Array Lean.ConstantInfo)

Find constants in current environment that match find options and predicate.

Equations

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

def Lean.getMatchingConstants.check {m : Type → Type} [Monad m] (p : Lean.ConstantInfo → m Bool) (matches_ : Array Lean.ConstantInfo) (_name : Lean.Name) (cinfo : Lean.ConstantInfo) : m (Array Lean.ConstantInfo)

Check constant should be returned

Equations

• Lean.getMatchingConstants.check p matches_ _name cinfo = do let include ← p cinfo if include = true then pure (matches_.push cinfo) else pure matches_