Aesop.Options.Public

source

inductive Aesop.Strategy :

Type

Search strategies which Aesop can use.

bestFirst : Strategy
Best-first search. This is the default strategy.
depthFirst : Strategy
Depth-first search. Whenever a rule is applied, Aesop immediately tries to solve each of its subgoals (from left to right), up to the maximum rule application depth. Goal and rule priorities are ignored, except to decide which rule is applied first.
breadthFirst : Strategy
Breadth-first search. Aesop always works on the oldest unsolved goal. Goal and rule priorities are ignored, except to decide which rule is applied first.

Instances For

source

instance Aesop.instInhabitedStrategy :

Inhabited Strategy

Equations

Aesop.instInhabitedStrategy = { default := Aesop.instInhabitedStrategy.default }

source

def Aesop.instInhabitedStrategy.default :

Strategy

Equations

Aesop.instInhabitedStrategy.default = Aesop.Strategy.bestFirst

Instances For

source

def Aesop.instBEqStrategy.beq :

Strategy → Strategy → Bool

Equations

Aesop.instBEqStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Aesop.instBEqStrategy :

BEq Strategy

Equations

Aesop.instBEqStrategy = { beq := Aesop.instBEqStrategy.beq }

source

instance Aesop.instReprStrategy :

Repr Strategy

Equations

Aesop.instReprStrategy = { reprPrec := Aesop.instReprStrategy.repr }

source

def Aesop.instReprStrategy.repr :

Strategy → Nat → Std.Format

Equations

Aesop.instReprStrategy.repr Aesop.Strategy.bestFirst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aesop.Strategy.bestFirst")).group prec✝
Aesop.instReprStrategy.repr Aesop.Strategy.depthFirst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aesop.Strategy.depthFirst")).group prec✝
Aesop.instReprStrategy.repr Aesop.Strategy.breadthFirst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aesop.Strategy.breadthFirst")).group prec✝

Instances For

source

structure Aesop.Options :

Type

Options which modify the behaviour of the aesop tactic.

strategy : Strategy
The search strategy used by Aesop.
maxRuleApplicationDepth : Nat
The maximum number of rule applications in any branch of the search tree (i.e., the maximum search depth). When a branch exceeds this limit, it is considered unprovable, but other branches may still be explored. 0 means no limit.
maxRuleApplications : Nat
Maximum total number of rule applications in the search tree. When this limit is exceeded, the search ends. 0 means no limit.
maxGoals : Nat
Maximum total number of goals in the search tree. When this limit is exceeded, the search ends. 0 means no limit.
maxNormIterations : Nat
Maximum number of norm rules applied to a single goal. When this limit is exceeded, normalisation is likely stuck in an infinite loop, so Aesop fails. 0 means no limit.
maxSafePrefixRuleApplications : Nat
When Aesop fails to prove a goal, it reports the goals that remain after safe rules have been applied exhaustively to the root goal, the safe descendants of the root goal, and so on (i.e., after the "safe prefix" of the search tree has been unfolded). However, it is possible for the search to fail before the safe prefix has been completely generated. In this case, Aesop expands the safe prefix after the fact. This option limits the number of additional rule applications generated during this process. 0 means no limit.
applyHypsTransparency : Lean.Meta.TransparencyMode
The transparency used by the applyHyps builtin rule. The rule applies a hypothesis h : T if T ≡ ∀ (x₁ : X₁) ... (xₙ : Xₙ), Y at the given transparency and if additionally the goal's target is defeq to Y at the given transparency.
assumptionTransparency : Lean.Meta.TransparencyMode
The transparency used by the assumption builtin rule. The rule applies a hypothesis h : T if T is defeq to the goal's target at the given transparency.
destructProductsTransparency : Lean.Meta.TransparencyMode
The transparency used by the destructProducts builtin rule. The rule splits a hypothesis h : T if T is defeq to a product-like type (e.g. T ≡ A ∧ B or T ≡ A × B) at the given transparency.
Note: we can index this rule only if the transparency is .reducible. With any other transparency, the rule becomes unindexed and is applied to every goal.
introsTransparency? : Option Lean.Meta.TransparencyMode
If this option is not none, the builtin intros rule unfolds the goal's target with the given transparency to discover ∀ binders. For example, with def T := ∀ x y : Nat, x = y, introsTransparency? := some .default and goal ⊢ T, the intros rule produces the goal x, y : Nat ⊢ x = y. With introsTransparency? := some .reducible, it produces ⊢ T. With introsTransparency? := none, it only introduces arguments which are syntactically bound by ∀ binders, so it also produces ⊢ T.
terminal : Bool
If true, Aesop succeeds only if it proves the goal. If false, Aesop always succeeds and reports the goals remaining after safe rules were applied.
warnOnNonterminal : Bool
If true, print a warning when Aesop does not prove the goal.
traceScript : Bool
If Aesop proves a goal and this option is true, Aesop prints a tactic proof as a Try this: suggestion.
enableSimp : Bool
Enable the builtin simp normalisation rule.
useSimpAll : Bool
Use simp_all, rather than simp at *, for the builtin simp normalisation rule.
useDefaultSimpSet : Bool
Use simp theorems from the default simp set, i.e. those tagged with @[simp]. If this option is false, Aesop uses only Aesop-specific simp theorems, i.e. those tagged with @[aesop simp]. Note that the congruence lemmas from the default simp set are always used.
enableUnfold : Bool
Enable the builtin unfold normalisation rule.