- kind : Lean.AttributeKind
- name : Lean.Name
- stx : Lean.Syntax
Equations
- Lean.Elab.instInhabitedAttribute = { default := { kind := default, name := default, stx := default } }
Equations
- Lean.Elab.instToFormatAttribute = { format := fun attr => let kindStr := match attr.kind with | Lean.AttributeKind.global => "" | Lean.AttributeKind.local => "local " | Lean.AttributeKind.scoped => "scoped " ; Lean.Format.bracket "@[" (Lean.format "" ++ Lean.format kindStr ++ Lean.format "" ++ Lean.format attr.name ++ Lean.format "" ++ Lean.format (toString attr.stx) ++ Lean.format "") "]" }
Equations
- Lean.Elab.toAttributeKind attrKindStx = if Lean.Syntax.isNone (Lean.Syntax.getOp attrKindStx 0) = true then pure Lean.AttributeKind.global else if (Lean.Syntax.getKind (Lean.Syntax.getOp (Lean.Syntax.getOp attrKindStx 0) 0) == `Lean.Parser.Term.scoped) = true then do let a ← Lean.Macro.getCurrNamespace let _do_jp : PUnit → Lean.MacroM Lean.AttributeKind := fun y => pure Lean.AttributeKind.scoped if Lean.Name.isAnonymous a = true then do let a ← Lean.getRef let y ← throw (Lean.Macro.Exception.error a "scoped attributes must be used inside namespaces") _do_jp y else do let y ← pure PUnit.unit _do_jp y else pure Lean.AttributeKind.local
Equations
- Lean.Elab.mkAttrKindGlobal = Lean.mkNode `Lean.Parser.Term.attrKind #[Lean.mkNullNode]
def
Lean.Elab.elabAttr
{m : Type → Type}
[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
- Lean.Elab.elabAttr attrInstance = do let attrKind ← Lean.Elab.liftMacroM (Lean.Elab.toAttributeKind (Lean.Syntax.getOp attrInstance 0)) let attr : Lean.Syntax := Lean.Syntax.getOp attrInstance 1 let attr ← Lean.Elab.liftMacroM (Lean.expandMacros attr) let _do_jp : Lean.Name → m Lean.Elab.Attribute := fun attrName => do let a ← Lean.getEnv let _do_jp : PUnit → m Lean.Elab.Attribute := fun y => pure { kind := attrKind, name := attrName, stx := attr } if Lean.isAttribute a attrName = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "unknown attribute [" ++ Lean.toMessageData attrName ++ Lean.toMessageData "]") _do_jp y if (Lean.Syntax.getKind attr == `Lean.Parser.Attr.simple) = true then do let y ← pure (Lean.Name.eraseMacroScopes (Lean.Syntax.getId (Lean.Syntax.getOp attr 0))) _do_jp y else match Lean.Syntax.getKind attr with | Lean.Name.str x s x_1 => do let y ← pure (Lean.Name.mkSimple s) _do_jp y | x => do let y ← Lean.throwErrorAt attr (Lean.toMessageData "unknown attribute") _do_jp y
def
Lean.Elab.elabAttrs
{m : Type → Type}
[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
- Lean.Elab.elabAttrs attrInstances = let attrs := #[]; do let r ← forIn attrInstances attrs fun attr r => let attrs := r; do let a ← Lean.Elab.elabAttr attr let attrs : Array Lean.Elab.Attribute := Array.push attrs a pure PUnit.unit pure (ForInStep.yield attrs) let x : Array Lean.Elab.Attribute := r let attrs : Array Lean.Elab.Attribute := x pure attrs
def
Lean.Elab.elabDeclAttrs
{m : Type → Type}
[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]
(stx : Lean.Syntax)
: