From ea55ec4090a84cc766d78fd4fd798b5fda614940 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Nov 2014 16:12:23 -0700 Subject: [PATCH] feat(frontends/lean/decl_cmds): remove useless name from 'example' commad --- src/frontends/lean/decl_cmds.cpp | 6 +++++- tests/lean/run/enum.lean | 2 +- tests/lean/run/example1.lean | 2 +- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index f2ab2cc32..80540a7fa 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -317,7 +317,11 @@ static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_op lean_assert(!(is_private && is_protected)); auto n_pos = p.pos(); unsigned start_line = n_pos.first; - name n = p.check_id_next("invalid declaration, identifier expected"); + name n; + if (kind == Example) + n = p.mk_fresh_name(); + else + n = p.check_id_next("invalid declaration, identifier expected"); decl_modifiers modifiers; name real_n; // real name for this declaration buffer ls_buffer; diff --git a/tests/lean/run/enum.lean b/tests/lean/run/enum.lean index 906ae00df..06c8b4476 100644 --- a/tests/lean/run/enum.lean +++ b/tests/lean/run/enum.lean @@ -10,7 +10,7 @@ namespace Three theorem disj (a : Three) : a = zero ∨ a = one ∨ a = two := rec (or.inl rfl) (or.inr (or.inl rfl)) (or.inr (or.inr rfl)) a - example ex1 (a : Three) : a ≠ zero → a ≠ one → a = two := + example (a : Three) : a ≠ zero → a ≠ one → a = two := rec (λ h₁ h₂, absurd rfl h₁) (λ h₁ h₂, absurd rfl h₂) (λ h₁ h₂, rfl) a end Three diff --git a/tests/lean/run/example1.lean b/tests/lean/run/example1.lean index 4d713c290..52a75a207 100644 --- a/tests/lean/run/example1.lean +++ b/tests/lean/run/example1.lean @@ -8,7 +8,7 @@ namespace day definition next_weekday d := rec_on d tuesday wednesday thursday friday monday monday monday - example test_next_weekday : next_weekday (next_weekday saturday) = tuesday := + example : next_weekday (next_weekday saturday) = tuesday := rfl end day