Tactics

The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.

aesop

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 }).

Tags:
Defined in module:: Aesop.Frontend.Tactic

aesop?

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 }).

Tags:
Defined in module:: Aesop.Frontend.Tactic