chore: remove comment from Linter

Old frontend is just providing `Syntax.missing`

src/Lean/Linter.lean

@@ -11,7 +11,7 @@ import Lean.Message
 
 namespace Lean
 
-def Linter := Environment → Name → /-Syntax → -/IO MessageLog
+def Linter := Environment → Name → Syntax → IO MessageLog
 
 def mkLintersRef : IO (IO.Ref (Array Linter)) :=
 IO.mkRef #[]

src/frontends/lean/definition_cmds.cpp

@@ -480,7 +480,7 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
         lean_assert(io_result_is_ok(r.raw()));
         array_ref<object *> linters(io_result_get_value(r.raw()), true);
         for (object * const & linter : linters) {
-            object * r2 = apply_3(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), io_mk_world());
+            object * r2 = apply_4(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), lean_box(0) /* Syntax.missing */, io_mk_world());
             consume_io_result(r2);
         }
 

tests/plugin/SnakeLinter.lean

@@ -5,7 +5,7 @@ open Lean
 def oh_no : Nat := 0
 
 def snakeLinter : Linter :=
-fun env n =>
+fun env n stx =>
   -- TODO(Sebastian): return actual message with position from syntax tree
   if n.toString.contains '_' then throw $ IO.userError "SNAKES!!"
   else pure MessageLog.empty