Documentation

Aesop.Frontend.Tactic

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

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.

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.
Equations
  • One or more equations did not get rendered due to their size.
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)) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.