Documentation

Lean.Elab.Attributes

structure Lean.Elab.Attribute :
Type
Equations
Equations
Equations
def Lean.Elab.elabAttr {m : TypeType} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadError m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] (attrInstance : Lean.Syntax) :
Equations
def Lean.Elab.elabAttrs {m : TypeType} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadError m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] (attrInstances : Array Lean.Syntax) :
Equations