class DocGen4.ValueAttr (attrKind : Type → Type) : Type 1

Captures the notion of a value based attributes, attrKind is things like EnumAttributes.

• getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Lean.Environment → Lean.Name → Option String

  Given a certain value based attribute, an Environment and the Name of a declaration returns the value of the attribute on this declaration if present.

structure DocGen4.ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] : Type 1

Contains a specific attribute declaration of a certain attribute kind (enum based, parametric etc.).

• α : Type
• attr : attrKind self.α
• str : ToString self.α
• inhab : Inhabited self.α

def DocGen4.enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : Lean.EnumAttributes α) (env : Lean.Environment) (decl : Lean.Name) : Option String

Obtain the value of an enum attribute for a certain name.

Equations

• DocGen4.enumGetValue attr env decl = do let val ← attr.getValue env decl some (toString val)

@[implicit_reducible]

instance DocGen4.instValueAttrEnumAttributes : ValueAttr Lean.EnumAttributes

Equations

• DocGen4.instValueAttrEnumAttributes = { getValue := fun {α : Type} [Inhabited α] [ToString α] => DocGen4.enumGetValue }

def DocGen4.parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : Lean.ParametricAttribute α) (env : Lean.Environment) (decl : Lean.Name) : Option String

Obtain the value of a parametric attribute for a certain name.

Equations

• DocGen4.parametricGetValue attr env decl = do let val ← attr.getParam? env decl some (attr.attr.name.toString ++ " " ++ toString val)

@[implicit_reducible]

instance DocGen4.instValueAttrParametricAttribute : ValueAttr Lean.ParametricAttribute

Equations

• DocGen4.instValueAttrParametricAttribute = { getValue := fun {α : Type} [Inhabited α] [ToString α] => DocGen4.parametricGetValue }

@[reducible, inline]

abbrev DocGen4.EnumAttrWrapper : Type 1

Equations

• DocGen4.EnumAttrWrapper = DocGen4.ValueAttrWrapper Lean.EnumAttributes

@[reducible, inline]

abbrev DocGen4.ParametricAttrWrapper : Type 1

Equations

• DocGen4.ParametricAttrWrapper = DocGen4.ValueAttrWrapper Lean.ParametricAttribute

def DocGen4.tagAttributes : Array Lean.TagAttribute

The list of all tag based attributes doc-gen knows about and can recover.

Equations

• DocGen4.tagAttributes = #[Lean.IR.UnboxResult.unboxAttr, Lean.neverExtractAttr, Lean.Elab.Term.elabWithoutExpectedTypeAttr, Lean.matchPatternAttr]

def DocGen4.instReprInlineAttributeKind_docGen4.repr : Lean.Compiler.InlineAttributeKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instReprInlineAttributeKind_docGen4 : Repr Lean.Compiler.InlineAttributeKind

Equations

• DocGen4.instReprInlineAttributeKind_docGen4 = { reprPrec := DocGen4.instReprInlineAttributeKind_docGen4.repr }

@[implicit_reducible]

instance DocGen4.instReprSpecializeAttributeKind_docGen4 : Repr Lean.Compiler.SpecializeAttributeKind

Equations

• DocGen4.instReprSpecializeAttributeKind_docGen4 = { reprPrec := DocGen4.instReprSpecializeAttributeKind_docGen4.repr }

def DocGen4.instReprSpecializeAttributeKind_docGen4.repr : Lean.Compiler.SpecializeAttributeKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instToStringInlineAttributeKind_docGen4 : ToString Lean.Compiler.InlineAttributeKind

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instToStringSpecializeAttributeKind_docGen4 : ToString Lean.Compiler.SpecializeAttributeKind

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instToStringReducibilityStatus_docGen4 : ToString Lean.ReducibilityStatus

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def DocGen4.enumAttributes : Array EnumAttrWrapper

The list of all enum based attributes doc-gen knows about and can recover.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instToStringExternEntry_docGen4 : ToString Lean.ExternEntry

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instToStringExternAttrData_docGen4 : ToString Lean.ExternAttrData

Equations

• DocGen4.instToStringExternAttrData_docGen4 = { toString := fun (data : Lean.ExternAttrData) => " ".intercalate (List.map toString data.entries) }

@[implicit_reducible]

instance DocGen4.instToStringDeprecationEntry_docGen4 : ToString Lean.Linter.DeprecationEntry

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.parametricAttributes : Array ParametricAttrWrapper

The list of all parametric attributes (that is, attributes with any kind of information attached) doc-gen knows about and can recover.

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.getTags (decl : Lean.Name) : Lean.MetaM (Array String)

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind] [Inhabited α] [ToString α] (decl : Lean.Name) (attr : attrKind α) : Lean.MetaM (Option String)

Equations

• DocGen4.getValuesAux decl attr = do let env ← Lean.getEnv pure (DocGen4.ValueAttr.getValue attr env decl)

def DocGen4.getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Lean.Name) (attrs : Array (ValueAttrWrapper attrKind)) : Lean.MetaM (Array String)

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.getEnumValues (decl : Lean.Name) : Lean.MetaM (Array String)

Equations

• DocGen4.getEnumValues decl = DocGen4.getValues decl DocGen4.enumAttributes

def DocGen4.getParametricValues (decl : Lean.Name) : Lean.MetaM (Array String)

Equations

• DocGen4.getParametricValues decl = DocGen4.getValues decl DocGen4.parametricAttributes

def DocGen4.getDefaultInstance (decl className : Lean.Name) : Lean.MetaM (Option String)

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.hasSimp (decl : Lean.Name) : Lean.MetaM (Option String)

Equations

• DocGen4.hasSimp decl = do let thms ← liftM Lean.Meta.simpExtension.getTheorems if thms.isLemma (Lean.Meta.Origin.decl decl) = true then pure (some "simp") else pure none

def DocGen4.hasCsimp (decl : Lean.Name) : Lean.MetaM (Option String)

Equations

• DocGen4.hasCsimp decl = do let env ← Lean.getEnv if Lean.Compiler.hasCSimpAttribute env decl = true then pure (some "csimp") else pure none

def DocGen4.getReducibility (decl : Lean.Name) : Lean.MetaM (Option String)

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.customAttrs : Array (Lean.Name → Lean.MetaM (Option String))

The list of custom attributes, that don't fit in the parametric or enum attribute kinds, doc-gen konws about and can recover.

Equations

• DocGen4.customAttrs = #[DocGen4.hasSimp, DocGen4.hasCsimp, DocGen4.getReducibility]

def DocGen4.getCustomAttrs (decl : Lean.Name) : Lean.MetaM (Array String)

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.getAllAttributes (decl : Lean.Name) : Lean.MetaM (Array String)

The main entry point for recovering all attribute values for a given declaration.

Equations

• One or more equations did not get rendered due to their size.