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
    @[reducible, inline]
    abbrev Lean.Elab.OpenDecl.M {m : Type → Type} (α : Type) :
    Type
    Equations
      Instances For
        source
        instance Lean.Elab.OpenDecl.instMonadResolveNameM {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
        MonadResolveName M
        Equations
          source
          def Lean.Elab.OpenDecl.resolveId {m : Type → Type} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddMessageContext m] [MonadLiftT (ST IO.RealWorld) m] (ns : Name) (idStx : Syntax) :
          M Name
          Equations
            Instances For
              source
              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] [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax `Lean.Parser.Command.openDecl) :
              m (List OpenDecl)
              Equations
                Instances For
                  source
                  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] [MonadResolveName m] (nss : List Name) (idStx : Ident) :
                  m Name
                  Equations
                    Instances For