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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Aesop.Frontend.Parser.«tactic_clause(Config:=_)» :
Lean.ParserDescr
Equations

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

Instances For

source
def Aesop.Frontend.Parser.«tactic_clause(Simp_config:=_)» :
Lean.ParserDescr
Equations

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

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

- Aesop.Frontend.elabOptions = Aesop.Frontend.elabOptions.unsafe_impl_3✝

Instances For

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

- Aesop.Frontend.elabSimpConfig = Aesop.Frontend.elabSimpConfig.unsafe_impl_3✝

Instances For

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

- Aesop.Frontend.elabSimpConfigCtx = Aesop.Frontend.elabSimpConfigCtx.unsafe_impl_3✝

Instances For

source
structure Aesop.Frontend.TacticConfig :
Type

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Aesop.Frontend.TacticConfig.getRuleSet (goal : Lean.MVarId) (c : TacticConfig) :
Lean.Elab.TermElabM LocalRuleSet
Equations

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

Instances For