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.
96 lines
1.8 KiB
Lean4
96 lines
1.8 KiB
Lean4
import Lean
|
|
|
|
/-!
|
|
This file tests that the convention for Lean block examples is correctly displayed in hovers.
|
|
|
|
Blocks that are indicated as output should be distinguished from blocks that are indicated as code
|
|
when hovers are shown. This is done by prefixing them with line comment markers.
|
|
|
|
This occurs only in hovers, so that other clients of this information can apply their own
|
|
conventions.
|
|
-/
|
|
|
|
/-!
|
|
# Ordinary Formatting
|
|
-/
|
|
|
|
/--
|
|
Does something complicated with IO that involves output.
|
|
|
|
```lean example
|
|
#eval complicatedIOProgram
|
|
```
|
|
```output
|
|
Hello!
|
|
More output
|
|
```
|
|
-/
|
|
def complicatedIOProgram : IO Unit := do
|
|
--^ textDocument/hover
|
|
IO.println "Hello!"
|
|
IO.println "More output"
|
|
|
|
|
|
/-!
|
|
# Indentation
|
|
These tests check the handling of indentation for output blocks
|
|
-/
|
|
|
|
/--
|
|
Does something complicated with IO that involves output.
|
|
|
|
```lean example
|
|
#eval anotherComplicatedIOProgram
|
|
```
|
|
|
|
```output
|
|
Hello!
|
|
More output
|
|
```
|
|
-/
|
|
def anotherComplicatedIOProgram : IO Unit := do
|
|
--^ textDocument/hover
|
|
IO.println "Hello!"
|
|
IO.println " More output"
|
|
|
|
/--
|
|
Does something complicated with IO that involves output.
|
|
|
|
```lean example
|
|
#eval yetAnotherComplicatedIOProgram
|
|
```
|
|
|
|
```output
|
|
Hello!
|
|
More output
|
|
```
|
|
-/
|
|
def yetAnotherComplicatedIOProgram : IO Unit := do
|
|
--^ textDocument/hover
|
|
IO.println "Hello!"
|
|
IO.println " More output"
|
|
|
|
|
|
/-!
|
|
# Programmatic Access
|
|
|
|
This test ensures that when looking up the docstring programmatically, the output blocks are not rewritten.
|
|
-/
|
|
|
|
/--
|
|
info: Does something complicated with IO that involves output.
|
|
|
|
```lean example
|
|
#eval complicatedIOProgram
|
|
```
|
|
```output
|
|
Hello!
|
|
More output
|
|
```
|
|
-/
|
|
#guard_msgs in
|
|
open Lean Elab Command in
|
|
#eval show CommandElabM Unit from do
|
|
let str ← Lean.findDocString? (← getEnv) ``complicatedIOProgram
|
|
str.forM (IO.println ·)
|