mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
62 lines
1.3 KiB
Lean4
62 lines
1.3 KiB
Lean4
|
|
|
|
|
|
/-!
|
|
Tests that docstring hovers are computed correctly for tactic extensions
|
|
-/
|
|
|
|
/-- Another `trivial` tactic -/
|
|
syntax (name := my_trivial) "my_trivial" : tactic
|
|
|
|
@[tactic_alt my_trivial]
|
|
syntax (name := very_trivial) "very_trivial" : tactic
|
|
macro_rules
|
|
| `(tactic|very_trivial) => `(tactic|my_trivial)
|
|
|
|
/-- It tries Lean's `trivial` -/
|
|
tactic_extension my_trivial
|
|
--^ textDocument/hover
|
|
macro_rules
|
|
| `(tactic|my_trivial) => `(tactic|trivial)
|
|
--^ textDocument/hover
|
|
|
|
/-- It tries `simp_all` -/
|
|
tactic_extension my_trivial
|
|
macro_rules
|
|
| `(tactic|my_trivial) => `(tactic|simp_all; done)
|
|
|
|
|
|
example : True := by
|
|
my_trivial
|
|
--^ textDocument/hover
|
|
|
|
/-- It tries `constructor` -/
|
|
tactic_extension my_trivial
|
|
--^ textDocument/hover
|
|
-- On the preceding line, it was not yet extended.
|
|
-- Here, it is:
|
|
macro_rules
|
|
| `(tactic|my_trivial) => `(tactic|constructor; done)
|
|
--^ textDocument/hover
|
|
|
|
/--
|
|
It tries some useful things:
|
|
* `omega`
|
|
* `simp_arith [*]`
|
|
-/
|
|
tactic_extension my_trivial
|
|
macro_rules
|
|
| `(tactic|my_trivial) => `(tactic|omega)
|
|
macro_rules
|
|
| `(tactic|my_trivial) => `(tactic|simp_arith [*]; done)
|
|
|
|
-- This tests that nested lists work
|
|
example : True := by
|
|
my_trivial
|
|
--^ textDocument/hover
|
|
|
|
-- This tests that alts are resolved
|
|
example : True := by
|
|
very_trivial
|
|
--^ textDocument/hover
|