feat(frontends/lean): add 'universes' command

src/emacs/lean-syntax.el

@@ -11,8 +11,8 @@
   '("import" "reducible" "irreducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
-    "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
-    "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
+    "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "universes"
+    "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
     "using" "namespace" "instance" "class" "section"
     "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")

src/frontends/lean/decl_cmds.cpp

@@ -24,9 +24,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 
 namespace lean {
-environment universe_cmd(parser & p) {
-    name n = p.check_id_next("invalid universe declaration, identifier expected");
-    environment env = p.env();
+static environment declare_universe(parser & p, environment env, name const & n) {
     if (in_section_or_context(env)) {
         p.add_local_level(n, mk_param_univ(n));
     } else {
@@ -39,6 +37,23 @@ environment universe_cmd(parser & p) {
     return env;
 }
 
+environment universe_cmd(parser & p) {
+    name n = p.check_id_next("invalid 'universe' command, identifier expected");
+    return declare_universe(p, p.env(), n);
+}
+
+environment universes_cmd(parser & p) {
+    if (!p.curr_is_identifier())
+        throw parser_error("invalid 'universes' command, identifier expected", p.pos());
+    environment env = p.env();
+    while (p.curr_is_identifier()) {
+        name n = p.get_name_val();
+        p.next();
+        env = declare_universe(p, env, n);
+    }
+    return env;
+}
+
 bool parse_univ_params(parser & p, buffer<name> & ps) {
     if (p.curr_is_token(get_llevel_curly_tk())) {
         p.next();
@@ -523,7 +538,8 @@ environment omit_cmd(parser & p) {
 }
 
 void register_decl_cmds(cmd_table & r) {
-    add_cmd(r, cmd_info("universe",     "declare a global universe level", universe_cmd));
+    add_cmd(r, cmd_info("universe",     "declare a universe level", universe_cmd));
+    add_cmd(r, cmd_info("universes",    "declare universe levels", universes_cmd));
     add_cmd(r, cmd_info("variable",     "declare a new variable", variable_cmd));
     add_cmd(r, cmd_info("parameter",    "declare a new parameter", parameter_cmd));
     add_cmd(r, cmd_info("constant",     "declare a new constant (aka top-level variable)", constant_cmd));

src/frontends/lean/token_table.cpp

@@ -83,7 +83,7 @@ void init_token_table(token_table & t) {
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible",
          "evaluate", "check", "eval", "[priority", "print", "end", "namespace", "section", "import",
-         "inductive", "record", "renaming", "extends", "structure", "module", "universe",
+         "inductive", "record", "renaming", "extends", "structure", "module", "universe", "universes",
          "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",

tests/lean/run/univs.lean

@@ -0,0 +1,9 @@
+import algebra.category.basic
+
+set_option pp.universes true
+section
+  universes l₁ l₂ l₃ l₄
+  parameter C : Category.{l₁ l₂}
+  parameter f : Category.{l₁ l₂} → Category.{l₃ l₄}
+  check f C
+end