Documentation

Lean.Elab.Open

source
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.

Instances For
    source
    @[inline]
    abbrev Lean.Elab.OpenDecl.M {m : Type → Type} (α : Type) :
    Type
    Equations
    source
    instance Lean.Elab.OpenDecl.instMonadResolveNameM {m : Type → Type} [inst : Monad m] [inst : MonadLiftT (ST IO.RealWorld) m] :
    Lean.MonadResolveName Lean.Elab.OpenDecl.M
    Equations
    • One or more equations did not get rendered due to their size.
    source
    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.
    source
    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] (stx : Lean.TSyntax `Lean.Parser.Command.openDecl) :
    m (List Lean.OpenDecl)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    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.Ident) :
    m Lean.Name
    Equations
    • One or more equations did not get rendered due to their size.