From d59bf05f20866c25aba82fea41e07c1b01b314c9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Nov 2016 11:53:21 -0800 Subject: [PATCH] feat(frontends/lean/scanner): allow ' in the beginning of identifiers --- src/frontends/lean/scanner.cpp | 2 +- tests/lean/run/tick_id.lean | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/tick_id.lean diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 60d52a3b3f..4013c1e576 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -435,7 +435,7 @@ void scanner::next_utf(buffer & cs) { } static bool is_id_first(buffer const & cs, unsigned i) { - if (std::isalpha(cs[i]) || cs[i] == '_') + if (std::isalpha(cs[i]) || cs[i] == '_' || cs[i] == '\'') return true; unsigned u = utf8_to_unicode(cs.begin() + i, cs.end()); return is_letter_like_unicode(u); diff --git a/tests/lean/run/tick_id.lean b/tests/lean/run/tick_id.lean new file mode 100644 index 0000000000..4282ff86bd --- /dev/null +++ b/tests/lean/run/tick_id.lean @@ -0,0 +1,9 @@ +def id₁ {'a : Type} (x : 'a) : 'a := x + +def id₂ {α : Type} (a : α) : α := a + +def id₃ {β : Type} (b : β) : β := b + +check λ (α β : Type) (f : α → β) (a : α), f a + +check λ ('a 'b : Type) (f : 'a → 'b) (a : 'a), f a