- kind : Lean.AttributeKind
- name : Lake.Name
- stx : Lean.Syntax
Instances For
attrKind := leading_parser optional («scoped» <|> «local»)
Instances For
def
Lean.Elab.elabAttr
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadResolveName m]
[Lean.MonadError m]
[Lean.Elab.MonadMacroAdapter m]
[Lean.MonadRecDepth m]
[Lean.MonadTrace m]
[Lean.MonadOptions m]
[Lean.AddMessageContext m]
[Lean.Elab.MonadInfoTree m]
[MonadLiftT IO m]
(attrInstance : Lean.Syntax)
:
Instances For
def
Lean.Elab.elabAttrs
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadResolveName m]
[Lean.MonadError m]
[Lean.Elab.MonadMacroAdapter m]
[Lean.MonadRecDepth m]
[Lean.MonadTrace m]
[Lean.MonadOptions m]
[Lean.AddMessageContext m]
[Lean.MonadLog m]
[Lean.Elab.MonadInfoTree m]
[MonadLiftT IO m]
(attrInstances : Array Lean.Syntax)
:
Instances For
def
Lean.Elab.elabDeclAttrs
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadResolveName m]
[Lean.MonadError m]
[Lean.Elab.MonadMacroAdapter m]
[Lean.MonadRecDepth m]
[Lean.MonadTrace m]
[Lean.MonadOptions m]
[Lean.AddMessageContext m]
[Lean.MonadLog m]
[Lean.Elab.MonadInfoTree m]
[MonadLiftT IO m]
(stx : Lean.Syntax)
: