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.
15 lines
506 B
Lean4
15 lines
506 B
Lean4
--^ waitForILeans
|
|
|
|
-- Regression test for a bug where (due to parallelism) the fvar ids weren't unique for the whole
|
|
-- module, leading to a conflict between `i` of `lt_next'` and the fvar id for `prev'`, thus
|
|
-- making go to definition jump to the wrong location.
|
|
|
|
theorem lt_next' (s : Substring.Raw) (i : String.Pos.Raw) (h : i.1 < s.bsize) :
|
|
i.1 < (s.next i).1 := by
|
|
sorry
|
|
|
|
def prev' : Substring.Raw → String.Pos.Raw → String.Pos.Raw := sorry
|
|
|
|
#check prev'
|
|
--^ textDocument/definition
|