Content-Length: 1041

{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":129,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n  for i in [0:100000] do\n    let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n    let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 <| .opaqueDecl {\n      name := name\n      levelParams := []\n      type := .const `Nat []\n      value := .const `Nat.zero []\n      isUnsafe := false\n      all := [name]\n    }\n    setEnv env'\n    addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}}