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.
3 lines
480 B
Plaintext
3 lines
480 B
Plaintext
Content-Length: 457
|
|
|
|
{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///test.lean","languageId":"lean","version":1,"text":"import Init.System.IO\n\ndef n : Nat := 1234\n\n#check n\n\ndef s : String := \"abcd\"\n\n#check s\n\ndef hello : IO Unit := IO.println \"Hello world!\"\n\n#eval hello\n\ndef αβγ /- 😉😉😉😉 -/: Nat := \"NotANat\"\n\nnamespace MyNs\n\ndef u : Unit := ()\n\nend MyNs\n\n#check MyNs.u\n\n#print MyNs.u\n"}}} |