import Lean.Elab

structure Bar where

structure Foo where
  foo₁ : Nat
  foo₂ : Nat
  bar  : Bar

def mkFoo₁ : Foo := {
--v textDocument/definition
  foo₁ := 1
--v textDocument/declaration
  foo₂ := 2
--v textDocument/typeDefinition
  bar := ⟨⟩
}

inductive HandWrittenStruct where
  | mk (n : Nat)

def HandWrittenStruct.n := fun | mk n => n

          --v textDocument/definition
def hws : HandWrittenStruct := {
--v textDocument/definition
  n := 3
}

            --v textDocument/declaration
def mkFoo₂ := mkFoo₁

syntax (name := elabTest) "test" : term

@[termElab elabTest] def elabElabTest : Lean.Elab.Term.TermElab := fun _ _ => do
  let stx ← `(2)
  Lean.Elab.Term.elabTerm stx none

     --v textDocument/declaration
#check test
     --^ textDocument/definition