From f06cdff2a17187fd5c59d6cb28ef1982fd16a636 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 4 Feb 2016 17:20:03 -0800 Subject: [PATCH] fix(library/blast/simplifier/ceqv): fix error in is_permutation --- src/library/blast/simplifier/ceqv.cpp | 4 ++-- tests/lean/run/perm_with_pi_args.lean | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/perm_with_pi_args.lean diff --git a/src/library/blast/simplifier/ceqv.cpp b/src/library/blast/simplifier/ceqv.cpp index 4c0d0f36e6..2123c7b126 100644 --- a/src/library/blast/simplifier/ceqv.cpp +++ b/src/library/blast/simplifier/ceqv.cpp @@ -207,9 +207,9 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset, return lhs == rhs; // locally bound variable } else if (var_idx(lhs) - offset < p.size()) { if (p[var_idx(lhs) - offset]) { - return *(p[var_idx(lhs) - offset]) == var_idx(rhs); + return *(p[var_idx(lhs) - offset]) == var_idx(rhs) - offset; } else { - p[var_idx(lhs) - offset] = var_idx(rhs); + p[var_idx(lhs) - offset] = var_idx(rhs) - offset; return true; } } else { diff --git a/tests/lean/run/perm_with_pi_args.lean b/tests/lean/run/perm_with_pi_args.lean new file mode 100644 index 0000000000..9370c22a6a --- /dev/null +++ b/tests/lean/run/perm_with_pi_args.lean @@ -0,0 +1,6 @@ +import data.matrix data.real data.fin +open matrix real + +axiom mx_add_comm {m n} (M₁ M₂ : matrix ℝ m n) : M₁ + M₂ = M₂ + M₁ +attribute mx_add_comm [simp] +example (m n : ℕ) (M₁ M₂ : matrix ℝ m n) : M₁ + M₂ = M₂ + M₁ := by simp