chore(library/init, frontends/lean): ensure old and new parser use the same command for initializing quotient module

lean4-mode/lean4-syntax.el

@@ -19,7 +19,7 @@
     "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
     "attributes" "raw" "replacing"
     "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
-    "exists" "if" "then" "else" "assume" "from"
+    "exists" "if" "then" "else" "assume" "from" "init_quot"
     "mutual" "def" "run_cmd")
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean4-keywords1-regexp

library/init/core.lean

@@ -203,7 +203,7 @@ constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α
 constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
   (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
 -/
-initQuot
+init_quot
 
 inductive Heq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
 | refl : Heq a

src/frontends/lean/builtin_cmds.cpp

@@ -407,7 +407,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("namespace",         "open a new namespace", namespace_cmd));
     add_cmd(r, cmd_info("end",               "close the current namespace/section", end_scoped_cmd));
     add_cmd(r, cmd_info("#check",            "type check given expression, and display its type", check_cmd));
-    add_cmd(r, cmd_info("initQuot",          "initialize `quot` type computational rules", init_quot_cmd));
+    add_cmd(r, cmd_info("init_quot",         "initialize `quot` type computational rules", init_quot_cmd));
     add_cmd(r, cmd_info("import",            "import module(s)", import_cmd));
     add_cmd(r, cmd_info("hide",              "hide aliases in the current scope", hide_cmd));
     register_decl_cmds(r);

src/frontends/lean/token_table.cpp

@@ -106,7 +106,7 @@ void init_token_table(token_table & t) {
          "import", "inductive", "coinductive", "structure", "class", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
          "set_option", "open", "export", "@[",
-         "attribute", "instance", "include", "omit", "initQuot",
+         "attribute", "instance", "include", "omit", "init_quot",
          "run_cmd", "#check", "#reduce", "#eval", "#print", "#help", "#exit",
          "#compile", "#unify", "#compact_tst", nullptr};