Documentation

Lean.Elab.Open

structure Lean.Elab.OpenDecl.State:

Type

openDecls : List Lean.OpenDecl
currNamespace : Lean.Name

@[inline]

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} [inst : Monad m] [inst : MonadLiftT (ST IO.RealWorld) m] :

Lean.MonadResolveName Lean.Elab.OpenDecl.M

Equations

Lean.Elab.OpenDecl.instMonadResolveNameM = { getCurrNamespace := do let a ← get pure a.currNamespace, getOpenDecls := do let a ← get pure a.openDecls }

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

Lean.Elab.OpenDecl.M Lean.Name

Equations

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

def Lean.Elab.OpenDecl.elabOpenDecl {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : MonadExceptOf Lean.Exception m] [inst : Lean.MonadRef m] [inst : Lean.AddMessageContext m] [inst : MonadLiftT (ST IO.RealWorld) m] [inst : Lean.MonadLog m] [inst : Lean.MonadResolveName m] (openDeclStx : Lean.Syntax) :

m (List Lean.OpenDecl)

Equations

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

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

Equations

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

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

Equations

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