From 3a72cd96218003c4986f53be200cb60bba01e9b4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Aug 2015 17:57:53 -0700 Subject: [PATCH] fix(frontends/lean): rename multiword keyword "suffices to show" to "suffices" --- library/data/hf.lean | 2 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_exprs.cpp | 6 ++---- src/frontends/lean/tokens.cpp | 4 ---- src/frontends/lean/tokens.h | 1 - src/frontends/lean/tokens.txt | 1 - tests/lean/run/suffices.lean | 4 ++-- 7 files changed, 6 insertions(+), 14 deletions(-) diff --git a/library/data/hf.lean b/library/data/hf.lean index 74983aede4..9169eda5d3 100644 --- a/library/data/hf.lean +++ b/library/data/hf.lean @@ -364,7 +364,7 @@ theorem insert_erase_subset (a : hf) (s : hf) : s ⊆ insert a (erase a s) := decidable.by_cases (assume ains : a ∈ s, by rewrite [!insert_erase ains]; apply subset.refl) (assume nains : a ∉ s, - suffices to show s ⊆ insert a s, by rewrite [erase_eq_of_not_mem nains]; assumption, + suffices s ⊆ insert a s, by rewrite [erase_eq_of_not_mem nains]; assumption, subset_insert s a) theorem insert_subset_insert (a : hf) {s t : hf} : s ⊆ t → insert a s ⊆ insert a t := diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 8cb09db783..c78b4c5735 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -20,7 +20,7 @@ "using" "namespace" "section" "fields" "find_decl" "attribute" "local" "set_option" "extends" "include" "omit" "classes" "instances" "coercions" "metaclasses" "raw" "migrate" "replacing" - "calc" "have" "show" "suffices" "to" "by" "in" "at" "let" "forall" "fun" + "calc" "have" "show" "suffices" "by" "in" "at" "let" "forall" "fun" "exists" "if" "dif" "then" "else" "assume" "assert" "take" "obtain" "from") "lean keywords ending with 'word' (not symbol)") diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index b046bc87bb..e66242859b 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -528,14 +528,12 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) } static expr parse_suffices_to_show(parser & p, unsigned, expr const *, pos_info const & pos) { - p.check_token_or_id_next(get_to_tk(), "invalid 'suffices to show' declaration, 'to' expected"); - p.check_token_next(get_show_tk(), "invalid 'suffices to show' declaration, 'show' expected"); auto prop_pos = p.pos(); expr from = p.parse_expr(); expr to = p.save_pos(mk_expr_placeholder(), prop_pos); expr prop = p.save_pos(mk_arrow(from, to), prop_pos); expr local = p.save_pos(mk_local(get_this_tk(), from), prop_pos); - p.check_token_next(get_comma_tk(), "invalid 'suffices to show' declaration, ',' expected"); + p.check_token_next(get_comma_tk(), "invalid 'suffices' declaration, ',' expected"); expr body; { parser::local_scope scope(p); @@ -543,7 +541,7 @@ static expr parse_suffices_to_show(parser & p, unsigned, expr const *, pos_info body = parse_proof(p, prop); } expr proof = p.save_pos(Fun(local, body), pos); - p.check_token_next(get_comma_tk(), "invalid 'suffices to show' declaration, ',' expected"); + p.check_token_next(get_comma_tk(), "invalid 'suffices' declaration, ',' expected"); expr rest = p.parse_expr(); expr r = p.mk_app(proof, rest, pos); return r; diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 55e279a6fe..c212c5d06b 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -50,7 +50,6 @@ static name const * g_assume_tk = nullptr; static name const * g_suppose_tk = nullptr; static name const * g_take_tk = nullptr; static name const * g_fun_tk = nullptr; -static name const * g_to_tk = nullptr; static name const * g_match_tk = nullptr; static name const * g_ellipsis_tk = nullptr; static name const * g_raw_tk = nullptr; @@ -203,7 +202,6 @@ void initialize_tokens() { g_suppose_tk = new name{"suppose"}; g_take_tk = new name{"take"}; g_fun_tk = new name{"fun"}; - g_to_tk = new name{"to"}; g_match_tk = new name{"match"}; g_ellipsis_tk = new name{"..."}; g_raw_tk = new name{"raw"}; @@ -357,7 +355,6 @@ void finalize_tokens() { delete g_suppose_tk; delete g_take_tk; delete g_fun_tk; - delete g_to_tk; delete g_match_tk; delete g_ellipsis_tk; delete g_raw_tk; @@ -510,7 +507,6 @@ name const & get_assume_tk() { return *g_assume_tk; } name const & get_suppose_tk() { return *g_suppose_tk; } name const & get_take_tk() { return *g_take_tk; } name const & get_fun_tk() { return *g_fun_tk; } -name const & get_to_tk() { return *g_to_tk; } name const & get_match_tk() { return *g_match_tk; } name const & get_ellipsis_tk() { return *g_ellipsis_tk; } name const & get_raw_tk() { return *g_raw_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index ab4978f224..e8d58538a5 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -52,7 +52,6 @@ name const & get_assume_tk(); name const & get_suppose_tk(); name const & get_take_tk(); name const & get_fun_tk(); -name const & get_to_tk(); name const & get_match_tk(); name const & get_ellipsis_tk(); name const & get_raw_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index 204d20c291..0d50302bfa 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -45,7 +45,6 @@ assume assume suppose suppose take take fun fun -to to match match ellipsis ... raw raw diff --git a/tests/lean/run/suffices.lean b/tests/lean/run/suffices.lean index 92435231f1..374a5dc359 100644 --- a/tests/lean/run/suffices.lean +++ b/tests/lean/run/suffices.lean @@ -1,6 +1,6 @@ variables {a b c : Prop} theorem foo (Ha : a) (Hab : a → b) (Hbc : b → c) : c := -suffices to show b, from Hbc this, -suffices to show a, from Hab this, +suffices b, from Hbc this, +suffices a, from Hab this, Ha