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

Equations

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

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

Equations

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

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 RuleExpr

@[implicit_reducible]

instance Aesop.Frontend.instInhabitedAttrConfig : Inhabited AttrConfig

Equations

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

def Aesop.Frontend.instInhabitedAttrConfig.default : AttrConfig

Equations

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

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

Equations

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