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

fix(library/simplifier): bug in is_permutation_ceqv

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-01 18:07:31 -07:00
parent 0fbc944cdd
commit 4ace996057
5 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/simplifier/ceqv.cpp
View file

@ -226,7 +226,7 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset,
bool is_permutation_ceqv(environment const & env, expr e) {
unsigned num_args = 0;
while (is_pi(e)) {
e = binding_domain(e);
e = binding_body(e);
num_args++;
}
expr lhs, rhs;

2
src/library/simplifier/rewrite_rule_set.cpp
View file

@ -28,7 +28,7 @@ format rewrite_rule::pp(formatter const & fmt) const {
r += format("#") + format(length(m_metas));
if (m_is_permutation)
r += space() + format("perm");
r += group(space() + fmt(m_lhs) + space() + format("↦") + pp_indent_expr(fmt, m_rhs));
r += group(comma() + space() + fmt(m_lhs) + space() + format("↦") + pp_indent_expr(fmt, m_rhs));
return r;
}

6
tests/lean/rw_set2.lean.expected.out
View file

@ -1,4 +1,4 @@
rewrite rules for eq
#1 g ?M_1 ↦ f ?M_1 + 1
#2 g ?M_1 ↦ 1
#2 f ?M_1 ↦ 0
#1, g ?M_1 ↦ f ?M_1 + 1
#2, g ?M_1 ↦ 1
#2, f ?M_1 ↦ 0

5
tests/lean/rw_set3.lean Normal file
View file

@ -0,0 +1,5 @@
import data.nat
attribute nat.add.comm [rewrite]
print [rewrite]

2
tests/lean/rw_set3.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
rewrite rules for eq
#2 perm, nat.add ?M_2 ?M_1 ↦ nat.add ?M_1 ?M_2