From defc2478b58f2abf64dfc711f4adb4c228a207aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Nov 2014 11:40:08 -0800 Subject: [PATCH] feat(frontends/lean): add 'record' as an alias for 'structure' command --- src/emacs/lean-syntax.el | 4 ++-- src/frontends/lean/token_table.cpp | 2 +- tests/lean/run/record8.lean | 6 ++++++ 3 files changed, 9 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/record8.lean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 0f3287f336..06d6875def 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -11,7 +11,7 @@ '("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" "example" - "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "universes" + "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "record" "universe" "universes" "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "calc_symm" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" @@ -105,7 +105,7 @@ (,(rx (or "λ" "→" "∃" "∀" ":=")) . 'font-lock-constant-face ) ;; universe/inductive/theorem... "names" (,(rx word-start - (group (or "inductive" "theorem" "axiom" "lemma" "hypothesis" "definition" "constant")) + (group (or "inductive" "structure" "record" "theorem" "axiom" "lemma" "hypothesis" "definition" "constant")) word-end (zero-or-more (or whitespace "(" "{" "[")) (group (zero-or-more (not (any " \t\n\r"))))) diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 753f6b461a..0577285741 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -95,7 +95,7 @@ void init_token_table(token_table & t) { pair cmd_aliases[] = {{"lemma", "theorem"}, {"corollary", "theorem"}, {"hypothesis", "parameter"}, {"conjecture", "parameter"}, - {nullptr, nullptr}}; + {"record", "structure"}, {nullptr, nullptr}}; auto it = builtin; while (it->first) { diff --git a/tests/lean/run/record8.lean b/tests/lean/run/record8.lean new file mode 100644 index 0000000000..36a8c2c907 --- /dev/null +++ b/tests/lean/run/record8.lean @@ -0,0 +1,6 @@ +import data.nat.basic + +record point := +(x y : nat) + +check point.x