summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/ExtractBase.ml72
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 ->
[