From c97092bef8428570d8ab737f03f63426bff075af Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Apr 2025 11:17:57 +1000 Subject: [PATCH] chore: omega calls assumption first (#7230) --- src/Lean/Elab/Tactic/Omega/Frontend.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index dd02db9c7d..d59eb84907 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -693,7 +693,9 @@ def omegaDefault : TacticM Unit := omegaTactic {} @[builtin_tactic Lean.Parser.Tactic.omega] def evalOmega : Tactic - | `(tactic| omega $cfg:optConfig) => do + | `(tactic| omega%$tk $cfg:optConfig) => do + -- Call `assumption` first, to avoid constructing unnecessary proofs. + withReducibleAndInstances (evalAssumption tk) <|> do let cfg ← elabOmegaConfig cfg omegaTactic cfg | _ => throwUnsupportedSyntax