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 <clause>* 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 <phase> <priority> <builder> <rule>) adds a rule. <phase> is unsafe, safe or norm. <priority> is a percentage for unsafe rules and an integer for safe and norm rules. <rule> is the name of a declaration or local hypothesis. <builder> is the rule builder used to turn <rule> into an Aesop rule. Example: (add unsafe 50% apply Or.inl).
• (erase <rule>) disables a globally registered Aesop rule. Example: (erase Aesop.BuiltinRules.assumption).
• (rule_sets [<ruleset>,*]) enables or disables named sets of rules for this Aesop call. Example: (rule_sets [-builtin, MyRuleSet]).
• (options { <opt> := <value> }) adjusts Aesop's search options. See Aesop.Options.
• (simp_options { <opt> := <value> }) 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 <clause>* 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 <phase> <priority> <builder> <rule>) adds a rule. <phase> is unsafe, safe or norm. <priority> is a percentage for unsafe rules and an integer for safe and norm rules. <rule> is the name of a declaration or local hypothesis. <builder> is the rule builder used to turn <rule> into an Aesop rule. Example: (add unsafe 50% apply Or.inl).
• (erase <rule>) disables a globally registered Aesop rule. Example: (erase Aesop.BuiltinRules.assumption).
• (rule_sets [<ruleset>,*]) enables or disables named sets of rules for this Aesop call. Example: (rule_sets [-builtin, MyRuleSet]).
• (options { <opt> := <value> }) adjusts Aesop's search options. See Aesop.Options.
• (simp_options { <opt> := <value> }) 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 : Lean.NameSet
• 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) : Lean.CoreM 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.