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(Config:=_)» : Lean.ParserDescr

Equations

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

def Aesop.Frontend.Parser.«tactic_clause(Simp_config:=_)» : 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]).
• (config { <opt> := <value> }) adjusts Aesop's search options. See Aesop.Options.
• (simp_config { <opt> := <value> }) adjusts options for Aesop's built-in simp rule. The given options are directly passed to simp. For example, (simp_config := { zeta := false }) makes Aesop use simp (config := { zeta := false }).

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]).
• (config { <opt> := <value> }) adjusts Aesop's search options. See Aesop.Options.
• (simp_config { <opt> := <value> }) adjusts options for Aesop's built-in simp rule. The given options are directly passed to simp. For example, (simp_config := { zeta := false }) makes Aesop use simp (config := { zeta := false }).

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 α

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

Equations

• Aesop.Frontend.elabOptions = Aesop.Frontend.elabOptions.unsafe_impl_1

def Aesop.Frontend.elabSimpConfig : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.Config

Equations

• Aesop.Frontend.elabSimpConfig = Aesop.Frontend.elabSimpConfig.unsafe_impl_1

def Aesop.Frontend.elabSimpConfigCtx : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.ConfigCtx

Equations

• Aesop.Frontend.elabSimpConfigCtx = Aesop.Frontend.elabSimpConfigCtx.unsafe_impl_1

structure Aesop.Frontend.TacticConfig : Type

• additionalRules : Array Aesop.Frontend.RuleExpr
• erasedRules : Array Aesop.Frontend.RuleExpr
• enabledRuleSets : Std.HashSet Aesop.RuleSetName
• options : Aesop.Options
• simpConfig : Lean.Meta.Simp.Config
• simpConfigSyntax? : Option Lean.Term

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

Equations

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

def Aesop.Frontend.TacticConfig.parse.go (goal : Lean.MVarId) (traceScript : Bool) (clauses : Array (Lean.TSyntax `Aesop.tactic_clause)) : Lean.Elab.TermElabM Aesop.Frontend.TacticConfig

Equations

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

def Aesop.Frontend.TacticConfig.parse.addClause (goal : Lean.MVarId) (traceScript : Bool) (stx : Lean.TSyntax `Aesop.tactic_clause) : StateRefT' IO.RealWorld Aesop.Frontend.TacticConfig Lean.Elab.TermElabM Unit

Equations

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

def Aesop.Frontend.TacticConfig.updateRuleSet (rs : Aesop.LocalRuleSet) (c : Aesop.Frontend.TacticConfig) (goal : Lean.MVarId) : Lean.Elab.TermElabM Aesop.LocalRuleSet

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.Elab.TermElabM Aesop.LocalRuleSet

Equations

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