lean4-htt/tests/server_interactive/completionEndSection.lean
Garmelon a3cb39eac9
chore: migrate more tests to new test suite (#12809)
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.
2026-03-06 16:52:01 +00:00

82 lines
1 KiB
Text

section
section Foo
end -- `Foo` expected
--^ completion
end
section
section Foo
end F -- `Foo` expected
--^ completion
end
section
section Foo
end B -- No completions expected
--^ completion
end
section
section Foo
section Bar
end -- `Bar` and `Foo.Bar` expected
--^ completion
end Foo
end
section
section Foo.Bar
end -- `Bar` and `Foo.Bar` expected
--^ completion
end Foo
end
section
section Foo
section Bar
end F -- `Foo.Bar` expected
--^ completion
end Foo
end
section
section Foo
section Bar
end B -- `Bar` expected
--^ completion
end Foo
end
section
section Foo
section Bar
end Foo. -- `Bar` expected
--^ completion
end
section
section Foo.Bar
end Foo.Bar
end -- No completions expected
--^ completion
section
section Foo.Bar.Geh
end Bar. -- `Geh` expected
--^ completion
end
section
section Foo
section
section Bar.Geh
end -- `Bar.Geh` and `Geh` expected
--^ completion
end
section
namespace Foo
namespace Bar
end Foo. -- `Bar` expected
--^ completion
end