structure Std.Tactic.Omega.OmegaConfig : Type

Configures the behaviour of the omega tactic.

• splitDisjunctions : Bool

  Split disjunctions in the context.

  Note that with splitDisjunctions := false omega will not be able to solve x = y goals as these are usually handled by introducing ¬ x = y as a hypothesis, then replacing this with x < y ∨ x > y.

  On the other hand, omega does not currently detect disjunctions which, when split, introduce no new useful information, so the presence of irrelevant disjunctions in the context can significantly increase run time.

• splitNatSub : Bool

  Whenever ((a - b : Nat) : Int) is found, register the disjunction b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0 for later splitting.

• splitNatAbs : Bool

  Whenever Int.natAbs a is found, register the disjunction 0 ≤ a ∧ Int.natAbs a = a ∨ a < 0 ∧ Int.natAbs a = - a for later splitting.

• splitMinMax : Bool

  Whenever min a b or max a b is found, rewrite in terms of the definition if a ≤ b ..., for later case splitting.

def Std.Tactic.Omega.elabOmegaConfig : Lean.Syntax → Lean.Elab.TermElabM Std.Tactic.Omega.OmegaConfig

Allow elaboration of OmegaConfig arguments to tactics.

Equations

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