max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/equations_compiler/structural_rec): "lemmas" ==> "equations"

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-02 11:17:38 -07:00
parent 691b200244
commit bf096eb292
5 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/equations_compiler/structural_rec.cpp
View file

@ -784,7 +784,7 @@ struct structural_rec_fn {
}
void mk_lemmas(expr const & fn, list<expr> 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) {

4
tests/lean/def_inaccessible_issue.lean
View file

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

4
tests/lean/def_inaccessible_issue.lean.expected.out
View file

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

2
tests/lean/eqn_sanitizer1.lean
View file

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

2
tests/lean/eqn_sanitizer1.lean.expected.out
View file

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