- openDecls : List Lean.OpenDecl
- currNamespace : Lean.Name
@[inline]
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
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)
:
Equations
- Lean.Elab.OpenDecl.resolveId ns idStx = let declName := ns ++ Lean.Syntax.getId idStx; do let a ← Lean.getEnv if Lean.Environment.contains a declName = true then pure declName else Lean.withRef idStx (Lean.resolveGlobalConstNoOverloadCore declName)
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.MonadResolveName m]
(openDeclStx : Lean.Syntax)
:
m (List Lean.OpenDecl)
Equations
- Lean.Elab.elabOpenDecl openDeclStx = do let a ← Lean.getOpenDecls let a_1 ← Lean.getCurrNamespace StateRefT'.run' (let _do_jp := fun y => do let a ← get pure a.openDecls; if (Lean.Syntax.getKind openDeclStx == `Lean.Parser.Command.openSimple) = true then do let y ← Lean.Elab.OpenDecl.elabOpenSimple openDeclStx _do_jp y else if (Lean.Syntax.getKind openDeclStx == `Lean.Parser.Command.openScoped) = true then do let y ← Lean.Elab.OpenDecl.elabOpenScoped openDeclStx _do_jp y else if (Lean.Syntax.getKind openDeclStx == `Lean.Parser.Command.openOnly) = true then do let y ← Lean.Elab.OpenDecl.elabOpenOnly openDeclStx _do_jp y else if (Lean.Syntax.getKind openDeclStx == `Lean.Parser.Command.openHiding) = true then do let y ← Lean.Elab.OpenDecl.elabOpenHiding openDeclStx _do_jp y else do let y ← Lean.Elab.OpenDecl.elabOpenRenaming openDeclStx _do_jp y) { openDecls := a, currNamespace := a_1 }
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
- Lean.Elab.resolveOpenDeclId ns idStx = do let a ← Lean.getOpenDecls let a_1 ← Lean.getCurrNamespace StateRefT'.run' (Lean.Elab.OpenDecl.resolveId ns idStx) { openDecls := a, currNamespace := a_1 }