def Lean.getMatchingConstants {m : Type → Type} [Monad m] [MonadEnv m] (p : ConstantInfo → m Bool) (includeImports : Bool := true) : m (Array 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 : ConstantInfo → m Bool) (matches_ : Array ConstantInfo) (_name : Name) (cinfo : ConstantInfo) : m (Array ConstantInfo)

Check constant should be returned

Equations

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