From fdd442bd38a237b0ec6f5e168284eea22da9082b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Nov 2015 11:41:56 -0800 Subject: [PATCH] feat(frontends/lean/decl_attributes): turn on `[forward]` if pattern hints have been provided --- src/frontends/lean/decl_attributes.cpp | 8 +++++++- tests/lean/run/pattern1.lean | 3 +-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 1ce6b0475..2ee998487 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -164,6 +164,12 @@ void decl_attributes::parse(parser & p) { } environment decl_attributes::apply(environment env, io_state const & ios, name const & d) const { + bool forward = m_forward; + if (has_pattern_hints(env.get(d).get_type())) { + // turn on [forward] if patterns hints have been used in the type. + forward = true; + } + if (m_is_instance) { if (m_priority) { #if defined(__GNUC__) && !defined(__CLANG__) @@ -233,7 +239,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c else env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, m_persistent); } - if (m_forward) { + if (forward) { if (m_priority) env = add_hi_lemma(env, ios.get_options(), d, *m_priority, m_persistent); else diff --git a/tests/lean/run/pattern1.lean b/tests/lean/run/pattern1.lean index 582bee9c8..581b444c7 100644 --- a/tests/lean/run/pattern1.lean +++ b/tests/lean/run/pattern1.lean @@ -5,11 +5,10 @@ sorry print lemma1 --- TODO(Leo): remove patterns that are permutations of of other patterns definition lemma2 [forward] {a b : nat} : f a b = f b a := sorry -definition lemma3 [forward] {a b : nat} : (:f a b:) = f b a := +definition lemma3 {a b : nat} : (:f a b:) = f b a := sorry print lemma2