feat(frontends/lean/token_table): add 'proposition' keyword

src/emacs/lean-syntax.el

@@ -11,7 +11,7 @@
   '("import" "prelude" "tactic_hint" "protected" "private" "noncomputable" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
-    "print" "theorem" "example" "abbreviation" "abstract"
+    "print" "theorem" "proposition" "example" "abbreviation" "abstract"
     "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"

src/frontends/lean/token_table.cpp

@@ -127,7 +127,7 @@ void init_token_table(token_table & t) {
          {g_qed_unicode, "qed"}, {nullptr, nullptr}};
 
     pair<char const *, char const *> cmd_aliases[] =
-        {{"lemma", "theorem"}, {"premise", "variable"}, {"premises", "variables"},
+        {{"lemma", "theorem"}, {"proposition", "theorem"}, {"premise", "variable"}, {"premises", "variables"},
          {"corollary", "theorem"}, {"hypothesis", "parameter"}, {"conjecture", "parameter"},
          {"record", "structure"}, {nullptr, nullptr}};
 

tests/lean/run/proposition.lean

@@ -0,0 +1,4 @@
+proposition tst {a b : Prop} : a → b → a ∧ b :=
+begin
+  intros, split, repeat assumption
+end