def Lean.Parser.Category.Aesop.attr_rules : Lean.Parser.Category

Equations

• Lean.Parser.Category.Aesop.attr_rules = { }

def Aesop.Frontend.Parser.Aesop.attr_rules.quot : Lean.ParserDescr

Equations

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

def Aesop.Frontend.Parser.attr_rules_ : Lean.ParserDescr

Equations

• Aesop.Frontend.Parser.attr_rules_ = Lean.ParserDescr.node `Aesop.Frontend.Parser.attr_rules_ 1022 (Lean.ParserDescr.cat `Aesop.rule_expr 0)

def Aesop.Frontend.Parser.«attr_rules[_]» : Lean.ParserDescr

Equations

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

def Aesop.Frontend.Parser.aesop : Lean.ParserDescr

Equations

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

structure Aesop.Frontend.AttrConfig : Type

• rules : Array Aesop.Frontend.RuleExpr

instance Aesop.Frontend.instInhabitedAttrConfig : Inhabited Aesop.Frontend.AttrConfig

Equations

• Aesop.Frontend.instInhabitedAttrConfig = { default := { rules := default } }

def Aesop.Frontend.AttrConfig.elab (stx : Lean.Syntax) : Lean.Elab.TermElabM Aesop.Frontend.AttrConfig

Equations

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