michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/decl_attributes): turn on [forward] if pattern hints have been provided

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-26 11:41:56 -08:00
parent c75e037b3c
commit fdd442bd38
2 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/decl_attributes.cpp
View file

@ -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

3
tests/lean/run/pattern1.lean
View file

@ -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