Skip to content

Commit 2c9641f

Browse files
authored
doc: modify aesop usage example of omegaDefault (#6549)
This PR fixes #6548.
1 parent 78ddee9 commit 2c9641f

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Elab/Tactic/Omega/Frontend.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -680,7 +680,7 @@ def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
680680

681681
/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
682682
`TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
683-
the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
683+
the tactic call `aesop (add 50% tactic Lean.Elab.Tactic.Omega.omegaDefault)`. -/
684684
def omegaDefault : TacticM Unit := omegaTactic {}
685685

686686
@[builtin_tactic Lean.Parser.Tactic.omega]

0 commit comments

Comments
 (0)