structure Lean.Elab.OpenDecl.State : Type

A local copy of name resolution state that allows us to immediately use new open decls in further name resolution as in open Lean Elab.

• openDecls : List OpenDecl
• currNamespace : Name

@[reducible, inline]

abbrev Lean.Elab.OpenDecl.M {m : Type → Type} (α : Type) : Type

instance Lean.Elab.OpenDecl.instMonadResolveNameM {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] : MonadResolveName M

def Lean.Elab.OpenDecl.resolveId {m : Type → Type} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] [AddMessageContext m] [MonadLog m] [MonadOptions m] [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name

def Lean.Elab.OpenDecl.resolveNameUsingNamespacesCore {m : Type → Type} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] [AddMessageContext m] [MonadLog m] [MonadOptions m] [MonadResolveName m] (nss : List Name) (idStx : Syntax) : m Name

Uniquely resolves the identifier idStx in the provided namespaces nss.

If the identifier does not indicate a name in exactly one of the namespaces, an exception is thrown.

def Lean.Elab.OpenDecl.elabOpenDecl {m : Type → Type} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddMessageContext m] [MonadLiftT (ST IO.RealWorld) m] [MonadLog m] [MonadOptions m] [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax `Lean.Parser.Command.openDecl) : m (List OpenDecl)

def Lean.Elab.OpenDecl.resolveNameUsingNamespaces {m : Type → Type} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddMessageContext m] [MonadLiftT (ST IO.RealWorld) m] [MonadLog m] [MonadOptions m] [MonadResolveName m] (nss : List Name) (idStx : Ident) : m Name