Merge pull request #146 from RaitoBezarius/main

fix(backends/lean): add a significant amount of keywords

1 files changed, 69 insertions, 3 deletions

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 8080e08c..f2686cc6 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -915,38 +915,104 @@ let keywords () =
         ]
     | Lean ->
         [
+          "Pi";
+          "Prop";
+          "Sort";
+          "Type";
+          "abbrev";
+          "alias";
+          "as";
+          "at";
+          "attribute";
+          "axiom";
+          "axioms";
+          "begin";
+          "break";
           "by";
+          "calc";
+          "catch";
           "class";
+          "const";
+          "constant";
+          "constants";
+          "continue";
           "decreasing_by";
           "def";
+          "definition";
           "deriving";
           "do";
           "else";
           "end";
+          "example";
+          "exists";
+          "export";
+          "extends";
           "for";
+          "forall";
+          "from";
+          "fun";
           "have";
+          "hiding";
           "if";
+          "import";
+          "in";
+          "include";
           "inductive";
+          "infix";
+          "infixl";
+          "infixr";
           "instance";
-          "import";
+          "lemma";
           "let";
+          "local";
           "macro";
+          "macro_rules";
           "match";
+          "mut";
+          "mutual";
           "namespace";
+          "noncomputable";
+          "notation";
+          "omit";
           "opaque";
+          "opaque_defs";
           "open";
+          "override";
+          "parameter";
+          "parameters";
+          "partial";
+          "postfix";
+          "precedence";
+          "prefix";
+          "prelude";
+          "private";
+          "protected";
+          "raw";
+          "record";
+          "reduce";
+          "renaming";
+          "replacing";
+          "reserve";
           "run_cmd";
+          "section";
           "set_option";
           "simp";
           "structure";
           "syntax";
           "termination_by";
           "then";
-          "Type";
+          "theorem";
+          "theory";
+          "universe";
+          "universes";
+          "unless";
           "unsafe";
+          "using";
+          "using_well_founded";
+          "variable";
+          "variables";
           "where";
           "with";
-          "opaque_defs";
         ]
     | HOL4 ->
         [