Documentation

Lean.ResolveName

@[inline]
abbrev Lean.AliasEntry :
Type
Equations
Equations
Equations
Equations
Equations
instance Lean.instMonadResolveName (m : TypeType) (n : TypeType) [inst : MonadLift m n] [inst : Lean.MonadResolveName m] :
Equations
def Lean.resolveGlobalName {m : TypeType} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] (id : Lean.Name) :
Equations
def Lean.resolveNamespace {m : TypeType} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Name) :
Equations
def Lean.resolveGlobalConstCore {m : TypeType} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (n : Lean.Name) :
Equations
def Lean.resolveGlobalConstNoOverloadCore {m : TypeType} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (n : Lean.Name) :
Equations
def Lean.resolveGlobalConst {m : TypeType} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] :
Equations
def Lean.resolveGlobalConstNoOverload {m : TypeType} [inst : Monad m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Syntax) :
Equations