def Lean.Parser.Category.Aesop.tactic_clause : Lean.Parser.Category

Equations

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

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

Equations

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

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

Equations

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

def Aesop.Frontend.Parser.«tactic_clause(Add_)» : Lean.ParserDescr

Equations

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

def Aesop.Frontend.Parser.«tactic_clause(Erase_)» : Lean.ParserDescr

Equations

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

def Aesop.Frontend.Parser.«tactic_clause(Rule_sets[_])» : Lean.ParserDescr

Equations

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

def Aesop.Frontend.Parser.«tactic_clause(Options:=_)» : Lean.ParserDescr

Equations

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

def Aesop.Frontend.Parser.«tactic_clause(Simp_options:=_)» : Lean.ParserDescr

Equations

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

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

aesop * tries to solve the current goal by applying a set of rules registered with the @[aesop] attribute. See its README for a tutorial and a reference.

The variant aesop? prints the proof it found as a Try this suggestion.

Clauses can be used to customise the behaviour of an Aesop call. Available clauses are:

• (add ) adds a rule. is unsafe, safe or norm. is a percentage for unsafe rules and an integer for safe and norm rules. is the name of a declaration or local hypothesis. is the rule builder used to turn into an Aesop rule. Example: (add unsafe 50% apply Or.inl).
• (erase ) disables a globally registered Aesop rule. Example: (erase Aesop.BuiltinRules.assumption).
• (rule_sets [,*]) enables or disables named sets of rules for this Aesop call. Example: (rule_sets [-builtin, MyRuleSet]).
• (options { := }) adjusts Aesop's search options. See Aesop.Options.
• (simp_options { := }) adjusts options for Aesop's built-in simp rule. See Aesop.SimpConfig.

Equations

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

def Aesop.Frontend.Parser.aesopTactic? : Lean.ParserDescr

aesop * tries to solve the current goal by applying a set of rules registered with the @[aesop] attribute. See its README for a tutorial and a reference.

The variant aesop? prints the proof it found as a Try this suggestion.

Clauses can be used to customise the behaviour of an Aesop call. Available clauses are:

• (add ) adds a rule. is unsafe, safe or norm. is a percentage for unsafe rules and an integer for safe and norm rules. is the name of a declaration or local hypothesis. is the rule builder used to turn into an Aesop rule. Example: (add unsafe 50% apply Or.inl).
• (erase ) disables a globally registered Aesop rule. Example: (erase Aesop.BuiltinRules.assumption).
• (rule_sets [,*]) enables or disables named sets of rules for this Aesop call. Example: (rule_sets [-builtin, MyRuleSet]).
• (options { := }) adjusts Aesop's search options. See Aesop.Options.
• (simp_options { := }) adjusts options for Aesop's built-in simp rule. See Aesop.SimpConfig.

Equations

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

unsafe def Aesop.Frontend.elabConfigUnsafe {α : Type} (type : Lean.Name) (stx : Lean.Syntax) : Lean.Elab.TermElabM α

Equations

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

unsafe def Aesop.Frontend.elabOptionsUnsafe : Lean.Syntax → Lean.Elab.TermElabM Aesop.Options

Equations

• Aesop.Frontend.elabOptionsUnsafe = Aesop.Frontend.elabConfigUnsafe `Aesop.Options

@[implemented_by Aesop.Frontend.elabOptionsUnsafe]

opaque Aesop.Frontend.elabOptions : Lean.Syntax → Lean.Elab.TermElabM Aesop.Options

unsafe def Aesop.Frontend.elabSimpConfigUnsafe : Lean.Syntax → Lean.Elab.TermElabM Aesop.SimpConfig

Equations

• Aesop.Frontend.elabSimpConfigUnsafe = Aesop.Frontend.elabConfigUnsafe `Aesop.SimpConfig

@[implemented_by Aesop.Frontend.elabSimpConfigUnsafe]

opaque Aesop.Frontend.elabSimpConfig : Lean.Syntax → Lean.Elab.TermElabM Aesop.SimpConfig

structure Aesop.Frontend.TacticConfig : Type

• additionalRules : Array Aesop.Frontend.RuleExpr
• erasedRules : Array Aesop.Frontend.RuleExpr
• enabledRuleSets : Array Aesop.RuleSetName
• options : Aesop.Options
• simpConfig : Aesop.SimpConfig
• simpConfigSyntax? : Option Lean.Term

def Aesop.Frontend.TacticConfig.parse (stx : Lean.Syntax) : Lean.Elab.TermElabM Aesop.Frontend.TacticConfig

Equations

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

def Aesop.Frontend.TacticConfig.parse.init (traceScript : Bool) : Aesop.Frontend.TacticConfig

Equations

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

def Aesop.Frontend.TacticConfig.parse.addClause (traceScript : Bool) (c : Aesop.Frontend.TacticConfig) (stx : Lean.Syntax) : Lean.Elab.TermElabM Aesop.Frontend.TacticConfig

Equations

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

def Aesop.Frontend.TacticConfig.updateRuleSets (goal : Lean.MVarId) (rss : Aesop.RuleSets) (c : Aesop.Frontend.TacticConfig) : Lean.MetaM (Lean.MVarId × Aesop.RuleSets)

Equations

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

def Aesop.Frontend.TacticConfig.getRuleSet (goal : Lean.MVarId) (c : Aesop.Frontend.TacticConfig) : Lean.MetaM (Lean.MVarId × Aesop.RuleSet)

Equations

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