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

chore(tests/lean): adjust tests to recent changes

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-20 19:08:41 -08:00
parent 4e6ad1d34d
commit f079d05fc2
8 changed files with 154 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,4 +1,4 @@
a + of_num b = 10 : Prop
(λ (x : ℕ), x) a + of_num b = 10 : Prop
@eq.{1} nat (@add.{1} nat nat.has_add ((λ (x : nat), x) a) (nat.of_num b))
(@bit0.{1} nat nat.has_add
(@bit1.{1} nat nat.has_one nat.has_add (@bit0.{1} nat nat.has_add (@one.{1} nat nat.has_one)))) :

2
tests/lean/pp_beta.lean
View file

@ -2,6 +2,6 @@ open nat
check (λ x : nat, x) 1
set_option pp.beta false
set_option pp.beta true
check (λ x : nat, x) 1

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

@ -1,2 +1,2 @@
1 : ℕ
(λ (x : ℕ), x) 1 : ℕ
1 : ℕ

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

@ -1,3 +1,3 @@
ind c ⟦a⟧ : B ⟦a⟧
ind c ⟦a⟧ : (λ (_x : quot s), B _x) ⟦a⟧
c a : B ⟦a⟧
c a

5
tests/lean/tactic_state_pp.lean.expected.out
View file

@ -1,8 +1,9 @@
tactic_state_pp.lean:31:0: error: tactic failed, there are unsolved goals
state:
My custom goal visualizer
Goal: ∀ {n_1 : ℕ} (a : α) (a_1 : Vec α n_1), n = nat.succ n_1 → v == Vec.cons a a_1 → f v ≠ 2
Goal: ∀ {n_1 : ℕ} (a : α) (a_1 : Vec α n_1),
(λ (a : ℕ) (w : Vec α a), n = a → v == w → f v ≠ 2) (nat.succ n_1) (Vec.cons a a_1)
tactic_state_pp.lean:39:0: error: tactic failed, there are unsolved goals
state:
My custom goal visualizer
Goal: ∀ (a : ℕ), n = succ a → 0 < n → succ (pred n) = n
Goal: ∀ (a : ℕ), (λ (w : ℕ), n = w → 0 < n → succ (pred n) = n) (succ a)

60
tests/lean/whnf.lean.expected.out
View file

@ -2,15 +2,27 @@ succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (succ a)), succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
0
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a),
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
(succ a)
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
2)
3
@ -18,15 +30,27 @@ succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (succ a)), succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
0
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a),
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
(succ a)
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
a)
succ a

30
tests/lean/whnf_cache_bug.lean.expected.out
View file

@ -3,14 +3,26 @@ nat.succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
0
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a),
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
(nat.succ a)
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
1)

120
tests/lean/whnf_core1.lean.expected.out
View file

@ -2,27 +2,51 @@ nat.succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
0
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a),
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
(nat.succ a)
(ih_1, poly_unit.star), ih_1, poly_unit.star))
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
0
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a),
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
(nat.succ a)
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
1), poly_unit.star))
a)
@ -30,27 +54,51 @@ nat.succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
0
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a),
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
(nat.succ a)
(ih_1, poly_unit.star), ih_1, poly_unit.star))
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
0
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (λ (a : ℕ), ℕ → ℕ) a × nat.below a),
((λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ),
(λ (a a_1 : ℕ) (_F : nat.below a_1),
nat.cases_on a_1 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
_F)
a_1
a
_F)
(nat.succ a)
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
1), poly_unit.star))
a)