From bf096eb2924ec6c1d583f3586048133b35273dec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Sep 2016 11:17:38 -0700 Subject: [PATCH] chore(library/equations_compiler/structural_rec): "lemmas" ==> "equations" --- src/library/equations_compiler/structural_rec.cpp | 2 +- tests/lean/def_inaccessible_issue.lean | 4 ++-- tests/lean/def_inaccessible_issue.lean.expected.out | 4 ++-- tests/lean/eqn_sanitizer1.lean | 2 +- tests/lean/eqn_sanitizer1.lean.expected.out | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index 1c5e2b11e1..c02de48d78 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -784,7 +784,7 @@ struct structural_rec_fn { } void mk_lemmas(expr const & fn, list const & lemmas) { - name base_name(const_name(get_app_fn(fn)), "lemmas"); + name base_name(const_name(get_app_fn(fn)), "equations"); unsigned eqn_idx = 1; type_context ctx = mk_type_context(); for (expr type : lemmas) { diff --git a/tests/lean/def_inaccessible_issue.lean b/tests/lean/def_inaccessible_issue.lean index eb0162b636..bb8a2a87e6 100644 --- a/tests/lean/def_inaccessible_issue.lean +++ b/tests/lean/def_inaccessible_issue.lean @@ -15,7 +15,7 @@ definition map2 : ∀ {n}, bv n → bv n → bv n | 0 nil nil := nil | (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2) -check map2._main.lemmas.eqn_2 +check map2._main.equations.eqn_2 set_option eqn_compiler.dsimp false @@ -25,4 +25,4 @@ definition map2' : ∀ {n}, bv n → bv n → bv n | 0 nil nil := nil | (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2' v1 v2) -check map2'._main.lemmas.eqn_2 +check map2'._main.equations.eqn_2 diff --git a/tests/lean/def_inaccessible_issue.lean.expected.out b/tests/lean/def_inaccessible_issue.lean.expected.out index 65efe3a96a..addac13e41 100644 --- a/tests/lean/def_inaccessible_issue.lean.expected.out +++ b/tests/lean/def_inaccessible_issue.lean.expected.out @@ -1,7 +1,7 @@ -map2._main.lemmas.eqn_2 : +map2._main.equations.eqn_2 : ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n), map2._main f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2._main f v1 v2) -map2'._main.lemmas.eqn_2 : +map2'._main.equations.eqn_2 : ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv (nat.rec n (λ (b₁ : ℕ), succ) 0)) (b2 : bool) (v2 : bv (nat.rec n (λ (b₁ : ℕ), succ) 0)), map2'._main f (cons (nat.rec n (λ (b₁ : ℕ), succ) 0) b1 v1) diff --git a/tests/lean/eqn_sanitizer1.lean b/tests/lean/eqn_sanitizer1.lean index 20bbbe7dc8..e8df314162 100644 --- a/tests/lean/eqn_sanitizer1.lean +++ b/tests/lean/eqn_sanitizer1.lean @@ -17,4 +17,4 @@ example : fib 0 = 1 := rfl example : fib 1 = 1 := rfl example (n : nat) : fib (n+2) = fib (n+1) + fib n := rfl -print fib._main.lemmas.eqn_3 +print fib._main.equations.eqn_3 diff --git a/tests/lean/eqn_sanitizer1.lean.expected.out b/tests/lean/eqn_sanitizer1.lean.expected.out index 5708f67162..ed7f7248a9 100644 --- a/tests/lean/eqn_sanitizer1.lean.expected.out +++ b/tests/lean/eqn_sanitizer1.lean.expected.out @@ -1,2 +1,2 @@ -definition fib._main.lemmas.eqn_3 : ∀ (n : ℕ), fib._main (n + 2) = fib._main (n + 1) + fib._main n := +definition fib._main.equations.eqn_3 : ∀ (n : ℕ), fib._main (n + 2) = fib._main (n + 1) + fib._main n := λ n, eq.refl (fib._main (nat.succ (nat.succ n)))