structure Lean.Elab.OpenDecl.State : Type

• openDecls : List Lean.OpenDecl
• currNamespace : Lake.Name

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.

@[inline, reducible]

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

Equations

• Lean.Elab.OpenDecl.M = StateRefT' IO.RealWorld Lean.Elab.OpenDecl.State m

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

Equations

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

def Lean.Elab.OpenDecl.resolveId {m : Type → Type} [Monad m] [Lean.MonadEnv m] [MonadExceptOf Lean.Exception m] [Lean.MonadRef m] [Lean.AddMessageContext m] [MonadLiftT (ST IO.RealWorld) m] (ns : Lake.Name) (idStx : Lean.Syntax) : Lean.Elab.OpenDecl.M Lake.Name

Equations

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

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

Equations

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

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

Equations

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