From cd6acb5d1d5dc59e0a7cfb49bfcc3333cd483bcf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Sep 2016 08:26:46 -0700 Subject: [PATCH] chore(library/pp_options): pp.binder_types true by default --- src/library/pp_options.cpp | 2 +- tests/lean/584a.lean.expected.out | 6 ++-- tests/lean/584b.lean.expected.out | 8 ++--- tests/lean/584c.lean.expected.out | 10 +++--- tests/lean/634d.lean.expected.out | 4 +-- tests/lean/652.lean.expected.out | 8 ++--- tests/lean/671.lean.expected.out | 2 +- tests/lean/acc.lean.expected.out | 4 ++- tests/lean/acc_rec_bug.lean.expected.out | 15 ++++++-- tests/lean/anc1.lean.expected.out | 36 +++++++++++-------- tests/lean/assert_tac3.lean.expected.out | 2 +- tests/lean/bug1.lean.expected.out | 14 ++++---- tests/lean/check.lean.expected.out | 2 +- tests/lean/choice_expl.lean.expected.out | 2 +- tests/lean/def3.lean.expected.out | 2 +- tests/lean/def4.lean.expected.out | 2 +- tests/lean/defeq_simp2.lean.expected.out | 2 +- tests/lean/elab12.lean.expected.out | 2 +- tests/lean/elab13.lean.expected.out | 10 +++--- tests/lean/elab15.lean.expected.out | 4 +-- tests/lean/eqn_sanitizer1.lean.expected.out | 2 +- tests/lean/eta_bug.lean.expected.out | 2 +- tests/lean/hole_issue2.lean.expected.out | 8 ++--- tests/lean/let1.lean.expected.out | 17 ++++----- tests/lean/nested1.lean.expected.out | 8 ++--- tests/lean/notation4.lean.expected.out | 8 ++--- tests/lean/omit.lean.expected.out | 4 +-- .../param_binder_update.lean.expected.out | 20 +++++------ .../param_binder_update2.lean.expected.out | 8 ++--- tests/lean/pattern_pp.lean.expected.out | 2 +- tests/lean/pp.lean.expected.out | 14 ++++---- tests/lean/pp_beta.lean.expected.out | 2 +- tests/lean/pp_binder_types.lean.expected.out | 4 +-- tests/lean/ppbug.lean.expected.out | 3 +- tests/lean/print_ax1.lean.expected.out | 6 ++-- tests/lean/print_ax2.lean.expected.out | 6 ++-- tests/lean/print_ax3.lean.expected.out | 6 ++-- .../lean/private_structure.lean.expected.out | 8 ++--- tests/lean/protected_test.lean.expected.out | 8 ++--- tests/lean/quot_bug.lean.expected.out | 2 +- tests/lean/rev_tac1.lean.expected.out | 2 +- tests/lean/sec_param_pp2.lean.expected.out | 2 +- .../simplifier_unsafe_nary.lean.expected.out | 2 +- tests/lean/struct_class.lean.expected.out | 4 +-- tests/lean/subpp.lean.expected.out | 2 +- tests/lean/t11.lean.expected.out | 6 ++-- tests/lean/t12.lean.expected.out | 2 +- tests/lean/t13.lean.expected.out | 2 +- tests/lean/univ_vars.lean.expected.out | 8 ++--- tests/lean/var2.lean.expected.out | 2 +- tests/lean/whnf.lean.expected.out | 4 +-- tests/lean/whnf_cache_bug.lean.expected.out | 2 +- tests/lean/whnf_core1.lean.expected.out | 4 +-- 53 files changed, 168 insertions(+), 149 deletions(-) diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 988c4fdffc..9bd4537004 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -84,7 +84,7 @@ Author: Leonardo de Moura #endif #ifndef LEAN_DEFAULT_PP_BINDER_TYPES -#define LEAN_DEFAULT_PP_BINDER_TYPES false +#define LEAN_DEFAULT_PP_BINDER_TYPES true #endif #ifndef LEAN_DEFAULT_PP_DELAYED_ABSTRACTION diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out index 886bfa8b8b..20737e6b36 100644 --- a/tests/lean/584a.lean.expected.out +++ b/tests/lean/584a.lean.expected.out @@ -1,5 +1,5 @@ -foo : Π A [H], A → A -foo' : Π {A} [H] {x}, A +foo : Π (A : Type) [H : inhabited A], A → A +foo' : Π {A : Type} [H : inhabited A] {x : A}, A foo ℕ 10 : ℕ definition test : ∀ {A : Type} [H : inhabited A], @foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5) = 10 := -λ A H, @rfl ℕ (@foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5)) +λ (A : Type) (H : inhabited A), @rfl ℕ (@foo' ℕ nat.is_inhabited (@has_add.add ℕ nat_has_add 5 5)) diff --git a/tests/lean/584b.lean.expected.out b/tests/lean/584b.lean.expected.out index 0a8f08edf0..6fd6153f00 100644 --- a/tests/lean/584b.lean.expected.out +++ b/tests/lean/584b.lean.expected.out @@ -1,4 +1,4 @@ -tst₁ : Π A, A → A -tst₂ : Π {A}, A → A -symm₂ : ∀ {A} a b, a = b → b = a -tst₃ : Π A, A → A +tst₁ : Π (A : Type), A → A +tst₂ : Π {A : Type}, A → A +symm₂ : ∀ {A : Type} (a b : A), a = b → b = a +tst₃ : Π (A : Type), A → A diff --git a/tests/lean/584c.lean.expected.out b/tests/lean/584c.lean.expected.out index 64fbacbbcd..e12d00ae68 100644 --- a/tests/lean/584c.lean.expected.out +++ b/tests/lean/584c.lean.expected.out @@ -1,5 +1,5 @@ -tst₁ : Π A, A → A -tst₂ : Π {A}, A → A -symm₂ : ∀ {A} a b, a = b → b = a -tst₃ : Π A, A → A -foo : ∀ {A} {a b}, a = b → ∀ c, c = b → c = a +tst₁ : Π (A : Type), A → A +tst₂ : Π {A : Type}, A → A +symm₂ : ∀ {A : Type} (a b : A), a = b → b = a +tst₃ : Π (A : Type), A → A +foo : ∀ {A : Type} {a b : A}, a = b → ∀ (c : A), c = b → c = a diff --git a/tests/lean/634d.lean.expected.out b/tests/lean/634d.lean.expected.out index 25ad1e93a8..52d9ff84cc 100644 --- a/tests/lean/634d.lean.expected.out +++ b/tests/lean/634d.lean.expected.out @@ -3,8 +3,8 @@ _root_.A : Type₁ → Type₁ A : Type.{l} → Type.{l} _root_.A.{1} : Type₁ → Type₁ P : B → B -_root_.P : Π {n}, ℕ → ℕ +_root_.P : Π {n : ℕ}, ℕ → ℕ P : B → B _root_.P.{1} : ?M_1 → ?M_1 @P 2 : B → B -@_root_.P.{1} ℕ : Π {n}, ℕ → ℕ +@_root_.P.{1} ℕ : Π {n : ℕ}, ℕ → ℕ diff --git a/tests/lean/652.lean.expected.out b/tests/lean/652.lean.expected.out index 0894bf4947..f4402e127c 100644 --- a/tests/lean/652.lean.expected.out +++ b/tests/lean/652.lean.expected.out @@ -1,6 +1,6 @@ -R : Π {b c}, Prop +R : Π {b c : bool}, Prop R2 : bool → bool → Prop R3 : bool → bool → Prop -R4 : bool → Π {c}, Prop -R5 : Π {b c}, Prop -R6 : Π {b}, bool → Prop +R4 : bool → Π {c : bool}, Prop +R5 : Π {b c : bool}, Prop +R6 : Π {b : bool}, bool → Prop diff --git a/tests/lean/671.lean.expected.out b/tests/lean/671.lean.expected.out index b531f34a54..54dd418b6a 100644 --- a/tests/lean/671.lean.expected.out +++ b/tests/lean/671.lean.expected.out @@ -1,2 +1,2 @@ protected definition nat.add : ℕ → ℕ → ℕ := -λ a b, nat.rec a (λ b₁ r, nat.succ r) b +λ (a b : ℕ), nat.rec a (λ (b₁ r : ℕ), nat.succ r) b diff --git a/tests/lean/acc.lean.expected.out b/tests/lean/acc.lean.expected.out index 3a125efe08..e903cd1abb 100644 --- a/tests/lean/acc.lean.expected.out +++ b/tests/lean/acc.lean.expected.out @@ -1,2 +1,4 @@ acc.rec : - Π {A} {R} {C}, (Π x, (∀ y, R y x → acc A R y) → (Π y, R y x → C y) → C x) → Π {a}, acc A R a → C a + Π {A : Type} {R : A → A → Prop} {C : A → Type}, + (Π (x : A), (∀ (y : A), R y x → acc A R y) → (Π (y : A), R y x → C y) → C x) → + Π {a : A}, acc A R a → C a diff --git a/tests/lean/acc_rec_bug.lean.expected.out b/tests/lean/acc_rec_bug.lean.expected.out index 4f14ebe726..2a8d7ac3a9 100644 --- a/tests/lean/acc_rec_bug.lean.expected.out +++ b/tests/lean/acc_rec_bug.lean.expected.out @@ -1,3 +1,12 @@ -F x₁ (λ y a, acc.rec (λ x₂ ac iH, F x₂ iH) (ac y a)) -acc.rec (λ x₂ ac iH, F x₂ iH) (acc.intro x₁ ac) : C x₁ -F x₁ (λ y a, acc.rec (λ x₂ ac iH, F x₂ iH) (ac y a)) : C x₁ +F x₁ + (λ (y : A) (a : R y x₁), + acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH) + (ac y a)) +acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH) + (acc.intro x₁ ac) : + C x₁ +F x₁ + (λ (y : A) (a : R y x₁), + acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH) + (ac y a)) : + C x₁ diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index 9c7e281394..e8d3b48226 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/tests/lean/anc1.lean.expected.out @@ -1,19 +1,25 @@ (1, 2) : ℕ × ℕ and.intro trivial trivial : true ∧ true -sigma.mk 1 sorry : Σ x, x > 0 +sigma.mk 1 sorry : Σ (x : ℕ), x > 0 show true, from true.intro : true -Exists.intro 1 (λ a, nat.no_confusion a) : ∃ x, 1 ≠ 0 -λ A B C Ha Hb Hc, show B ∧ A, from and.intro Hb Ha : ∀ A B C, A → B → C → B ∧ A -λ A B C Ha Hb Hc, show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) : - ∀ A B C, A → B → C → B ∧ A ∧ C ∧ A -λ A B C Ha Hb Hc, show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) : - ∀ A B C, A → B → C → B ∧ A ∧ C ∧ A -λ A B C Ha Hb Hc, +Exists.intro 1 (λ (a : 1 = 0), nat.no_confusion a) : ∃ (x : ℕ), 1 ≠ 0 +λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha : + ∀ (A B C : Prop), A → B → C → B ∧ A +λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), + show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) : + ∀ (A B C : Prop), A → B → C → B ∧ A ∧ C ∧ A +λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), + show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) : + ∀ (A B C : Prop), A → B → C → B ∧ A ∧ C ∧ A +λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show ((B ∧ true) ∧ A) ∧ C ∧ A, from and.intro (and.intro (and.intro Hb true.intro) Ha) (and.intro Hc Ha) : - ∀ A B C, A → B → C → ((B ∧ true) ∧ A) ∧ C ∧ A -λ A P Q a H1 H2, show ∃ x, P x ∧ Q x, from Exists.intro a (and.intro H1 H2) : - ∀ A P Q a, P a → Q a → (∃ x, P x ∧ Q x) -λ A P Q a b H1 H2, show ∃ x y, P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) : - ∀ A P Q a b, P a → Q b → (∃ x y, P x ∧ Q y) -λ A P Q a b H1 H2, show ∃ x y, P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) : - ∀ A P Q a b, P a → Q b → (∃ x y, P x ∧ Q y) + ∀ (A B C : Prop), A → B → C → ((B ∧ true) ∧ A) ∧ C ∧ A +λ (A : Type) (P Q : A → Prop) (a : A) (H1 : P a) (H2 : Q a), + show ∃ (x : A), P x ∧ Q x, from Exists.intro a (and.intro H1 H2) : + ∀ (A : Type) (P Q : A → Prop) (a : A), P a → Q a → (∃ (x : A), P x ∧ Q x) +λ (A : Type) (P Q : A → Prop) (a b : A) (H1 : P a) (H2 : Q b), + show ∃ (x y : A), P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) : + ∀ (A : Type) (P Q : A → Prop) (a b : A), P a → Q b → (∃ (x y : A), P x ∧ Q y) +λ (A : Type) (P Q : A → Prop) (a b : A) (H1 : P a) (H2 : Q b), + show ∃ (x y : A), P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) : + ∀ (A : Type) (P Q : A → Prop) (a b : A), P a → Q b → (∃ (x y : A), P x ∧ Q y) diff --git a/tests/lean/assert_tac3.lean.expected.out b/tests/lean/assert_tac3.lean.expected.out index 24a56f4c00..278d9da1d1 100644 --- a/tests/lean/assert_tac3.lean.expected.out +++ b/tests/lean/assert_tac3.lean.expected.out @@ -5,7 +5,7 @@ x : ℕ := ?m_1 a : ℕ ⊢ ℕ definition tst2 : ∀ (a : ℕ), a = a := -λ a, let x : ℕ := a in eq.refl a +λ (a : ℕ), let x : ℕ := a in eq.refl a a b : ℕ, x : ℕ := ?m_1 ⊢ a = a diff --git a/tests/lean/bug1.lean.expected.out b/tests/lean/bug1.lean.expected.out index 1e8f3bac71..36882a546c 100644 --- a/tests/lean/bug1.lean.expected.out +++ b/tests/lean/bug1.lean.expected.out @@ -1,13 +1,13 @@ bug1.lean:9:7: error: type mismatch at definition 'and_intro1', has type - ∀ p q, p → q → ∀ c, (p → q → c) → c + ∀ (p q : bool), p → q → ∀ (c : bool), (p → q → c) → c but is expected to have type - ∀ p q, p → q → a + ∀ (p q : bool), p → q → a bug1.lean:13:7: error: type mismatch at definition 'and_intro2', has type - ∀ p q, p → q → ∀ c, (p → q → c) → c + ∀ (p q : bool), p → q → ∀ (c : bool), (p → q → c) → c but is expected to have type - ∀ p q, p → q → p ∧ p + ∀ (p q : bool), p → q → p ∧ p bug1.lean:17:7: error: type mismatch at definition 'and_intro3', has type - ∀ p q, p → q → ∀ c, (p → q → c) → c + ∀ (p q : bool), p → q → ∀ (c : bool), (p → q → c) → c but is expected to have type - ∀ p q, p → q → q ∧ p -and_intro4 : ∀ p q, p → q → p ∧ q + ∀ (p q : bool), p → q → q ∧ p +and_intro4 : ∀ (p q : bool), p → q → p ∧ q diff --git a/tests/lean/check.lean.expected.out b/tests/lean/check.lean.expected.out index da7cf850df..1fc5b28442 100644 --- a/tests/lean/check.lean.expected.out +++ b/tests/lean/check.lean.expected.out @@ -1,4 +1,4 @@ and.intro : ?M_1 → ?M_2 → ?M_1 ∧ ?M_2 or.elim : ?M_1 ∨ ?M_2 → (?M_1 → ?M_3) → (?M_2 → ?M_3) → ?M_3 eq : ?M_1 → ?M_1 → Prop -eq.rec : ?M_3 ?M_2 → Π {a}, ?M_2 = a → ?M_3 a +eq.rec : ?M_3 ?M_2 → Π {a : ?M_1}, ?M_2 = a → ?M_3 a diff --git a/tests/lean/choice_expl.lean.expected.out b/tests/lean/choice_expl.lean.expected.out index a99dbd0c7b..5916e0c70a 100644 --- a/tests/lean/choice_expl.lean.expected.out +++ b/tests/lean/choice_expl.lean.expected.out @@ -1,4 +1,4 @@ -pr : Π {A}, A → A → A +pr : Π {A : Type}, A → A → A pr a b : N choice_expl.lean:14:6: error: ambiguous overload, possible interpretations N2.pr a b diff --git a/tests/lean/def3.lean.expected.out b/tests/lean/def3.lean.expected.out index 150032416a..345a262b86 100644 --- a/tests/lean/def3.lean.expected.out +++ b/tests/lean/def3.lean.expected.out @@ -1 +1 @@ -f : Π A, A → A +f : Π (A : Type), A → A diff --git a/tests/lean/def4.lean.expected.out b/tests/lean/def4.lean.expected.out index 01b7beb2f2..87d4cbd46c 100644 --- a/tests/lean/def4.lean.expected.out +++ b/tests/lean/def4.lean.expected.out @@ -16,6 +16,6 @@ has type ℕ but is expected to have type A -f : Π A, A → A +f : Π (A : Type), A → A f ℕ 0 : ℕ g 0 : ℕ diff --git a/tests/lean/defeq_simp2.lean.expected.out b/tests/lean/defeq_simp2.lean.expected.out index ba51b40230..3aca76b0ea 100644 --- a/tests/lean/defeq_simp2.lean.expected.out +++ b/tests/lean/defeq_simp2.lean.expected.out @@ -1,4 +1,4 @@ f a (foo1 a) = f a (foo2 a) f a (foo1 a) = f a (foo1 a) f a (foo2 a) = f a (foo2 a) -(λ x, f x (id (id (id (foo1 x))))) = λ x, f x (foo2 x) +(λ (x : ℕ), f x (id (id (id (foo1 x))))) = λ (x : ℕ), f x (foo2 x) diff --git a/tests/lean/elab12.lean.expected.out b/tests/lean/elab12.lean.expected.out index e46c0a9b3a..7f480b04fa 100644 --- a/tests/lean/elab12.lean.expected.out +++ b/tests/lean/elab12.lean.expected.out @@ -10,4 +10,4 @@ but is expected to have type a = a elab12.lean:11:2: error: function expected at H -λ a, have H : a = a, from rfl, H : ∀ a, a = a +λ (a : ℕ), have H : a = a, from rfl, H : ∀ (a : ℕ), a = a diff --git a/tests/lean/elab13.lean.expected.out b/tests/lean/elab13.lean.expected.out index a5e044e7dc..8dd3b6579a 100644 --- a/tests/lean/elab13.lean.expected.out +++ b/tests/lean/elab13.lean.expected.out @@ -1,6 +1,6 @@ -λ c, - get_env >>= λ env, - returnex (environment.get env c) >>= λ decl, - return (length (declaration.univ_params decl)) >>= λ num, - mk_num_meta_univs 2 >>= λ ls, return (expr.const c ls) : +λ (c : name), + get_env >>= λ (env : environment), + returnex (environment.get env c) >>= λ (decl : declaration), + return (length (declaration.univ_params decl)) >>= λ (num : ℕ), + mk_num_meta_univs 2 >>= λ (ls : list level), return (expr.const c ls) : name → tactic expr diff --git a/tests/lean/elab15.lean.expected.out b/tests/lean/elab15.lean.expected.out index e0110b0ef1..5a731574de 100644 --- a/tests/lean/elab15.lean.expected.out +++ b/tests/lean/elab15.lean.expected.out @@ -1,4 +1,4 @@ -λ A a b c d H₁ H₂ H₃, +λ (A : Type) (a b c d : A) (H₁ : eq a b) (H₂ : eq c b) (H₃ : eq d c), have this : eq a c, from eq.trans H₁ (eq.symm H₂), show eq a d, from eq.trans this (eq.symm H₃) : - ∀ A a b c d, eq a b → eq c b → eq d c → eq a d + ∀ (A : Type) (a b c d : A), eq a b → eq c b → eq d c → eq a d diff --git a/tests/lean/eqn_sanitizer1.lean.expected.out b/tests/lean/eqn_sanitizer1.lean.expected.out index 6e8b5b0779..1f54dbfeeb 100644 --- a/tests/lean/eqn_sanitizer1.lean.expected.out +++ b/tests/lean/eqn_sanitizer1.lean.expected.out @@ -1,2 +1,2 @@ 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 n) + fib._main n) +λ (n : ℕ), eq.refl (fib._main (nat.succ n) + fib._main n) diff --git a/tests/lean/eta_bug.lean.expected.out b/tests/lean/eta_bug.lean.expected.out index 9f16993599..6ce8ac64d8 100644 --- a/tests/lean/eta_bug.lean.expected.out +++ b/tests/lean/eta_bug.lean.expected.out @@ -1 +1 @@ -λ A x y H₁ H₂, eq.rec H₁ H₂ +λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.rec H₁ H₂ diff --git a/tests/lean/hole_issue2.lean.expected.out b/tests/lean/hole_issue2.lean.expected.out index 60962e3b27..8d08f27132 100644 --- a/tests/lean/hole_issue2.lean.expected.out +++ b/tests/lean/hole_issue2.lean.expected.out @@ -3,7 +3,7 @@ state: A : Type, b₁ b₂ : bag A, l₁ l₂ : list A, -_match : Π b, subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦l₂⟧), +_match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦l₂⟧), H : subcount l₁ l₂ = ff, h : ⟦l₁⟧ ⊆ ⟦l₂⟧, w : A, @@ -14,16 +14,16 @@ state: A : Type, b₁ b₂ : bag A, l₁ l₂ : list A, -_match : Π b, subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦l₂⟧), +_match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦l₂⟧), H : subcount l₁ l₂ = ff, h : ⟦l₁⟧ ⊆ ⟦l₂⟧ -⊢ ∀ a, ¬list.count a l₁ ≤ list.count a l₂ → false +⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false hole_issue2.lean:37:28: error: don't know how to synthesize placeholder state: A : Type, b₁ b₂ : bag A, l₁ l₂ : list A, -_match : Π b, subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦l₂⟧), +_match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦l₂⟧), H : subcount l₁ l₂ = ff, h : ⟦l₁⟧ ⊆ ⟦l₂⟧ ⊢ false diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out index 73082948ac..99ced77ee5 100644 --- a/tests/lean/let1.lean.expected.out +++ b/tests/lean/let1.lean.expected.out @@ -1,13 +1,14 @@ let bool : Type := Prop, - and : bool → bool → Prop := λ p q, Π c, (p → q → c) → c, - and_intro : Π p q, p → q → and p q := λ p q H1 H2 c H, H H1 H2, - and_elim_left : Π p q, and p q → p := λ p q H, H p (λ H1 H2, H1), - and_elim_right : Π p q, and p q → q := λ p q H, H q (λ H1 H2, H2) + and : bool → bool → Prop := λ (p q : bool), Π (c : bool), (p → q → c) → c, + and_intro : Π (p q : bool), p → q → and p q := + λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2, + and_elim_left : Π (p q : bool), and p q → p := λ (p q : bool) (H : and p q), H p (λ (H1 : p) (H2 : q), H1), + and_elim_right : Π (p q : bool), and p q → q := λ (p q : bool) (H : and p q), H q (λ (H1 : p) (H2 : q), H2) in and_intro : - ∀ p q, p → q → ∀ c, (p → q → c) → c + ∀ (p q : Prop), p → q → ∀ (c : Prop), (p → q → c) → c let1.lean:20:19: error: invalid let-expression, expression - λ p q H1 H2 c H, H H1 H2 + λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2 has type - Π p q, p → q → Π c, (p → q → c) → c + Π (p q : bool), p → q → Π (c : bool), (p → q → c) → c but is expected to have type - Π p q, p → q → and q p + Π (p q : bool), p → q → and q p diff --git a/tests/lean/nested1.lean.expected.out b/tests/lean/nested1.lean.expected.out index 5703c84221..f6e8e9e0ea 100644 --- a/tests/lean/nested1.lean.expected.out +++ b/tests/lean/nested1.lean.expected.out @@ -1,10 +1,10 @@ attribute [irreducible] definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) := -λ x, lt.step (zero_lt_succ x) +λ (x : ℕ), lt.step (zero_lt_succ x) noncomputable definition test.bla : ℕ → ℕ := -λ a, foo (succ (succ a)) (foo.prf a) +λ (a : ℕ), foo (succ (succ a)) (foo.prf a) noncomputable definition test.bla : ℕ → ℕ := -λ a, test.foo (succ (succ a)) (test.foo.prf a) +λ (a : ℕ), test.foo (succ (succ a)) (test.foo.prf a) attribute [irreducible] definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) := -λ x, lt.step (zero_lt_succ x) +λ (x : ℕ), lt.step (zero_lt_succ x) diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out index 91a855b2c2..8f564d9e20 100644 --- a/tests/lean/notation4.lean.expected.out +++ b/tests/lean/notation4.lean.expected.out @@ -1,4 +1,4 @@ -∃ A x y, x = y : Prop -∃ x, x = 0 : Prop -Σ x, x = 10 : Type₁ -Σ A, List A : Type₂ +∃ (A : Type₁) (x y : A), x = y : Prop +∃ (x : num), x = 0 : Prop +Σ (x : num), x = 10 : Type₁ +Σ (A : Type₁), List A : Type₂ diff --git a/tests/lean/omit.lean.expected.out b/tests/lean/omit.lean.expected.out index db36495ce4..892cd5e9e0 100644 --- a/tests/lean/omit.lean.expected.out +++ b/tests/lean/omit.lean.expected.out @@ -1,4 +1,4 @@ omit.lean:5:7: error: invalid omit command, 'A' has not been included omit.lean:7:10: error: invalid include command, 'A' has already been included -foo : Π A, A → A → Π B, B → B -tst : Π A, A → A → Type → Type +foo : Π (A : Type), A → A → Π (B : Type), B → B +tst : Π (A : Type), A → A → Type → Type diff --git a/tests/lean/param_binder_update.lean.expected.out b/tests/lean/param_binder_update.lean.expected.out index 277f9f4975..0e1e631150 100644 --- a/tests/lean/param_binder_update.lean.expected.out +++ b/tests/lean/param_binder_update.lean.expected.out @@ -1,17 +1,17 @@ -id : Π {A}, A → A -id₂ : Π {A}, A → A +id : Π {A : Type}, A → A +id₂ : Π {A : Type}, A → A foo1 : A → B → A foo2 : A → B → A foo3 : A → B → A foo4 : A → B → A -foo1 : Π {A} {B}, A → B → A -foo2 : Π {A} B, A → B → A -foo3 : Π A {B}, A → B → A -foo4 : Π A B, A → B → A -boo1 : Π {A} {B}, A → B → A -boo2 : Π {A} B, A → B → A -boo3 : Π A {B}, A → B → A -boo4 : Π A B, A → B → A +foo1 : Π {A : Type} {B : Type}, A → B → A +foo2 : Π {A : Type} (B : Type), A → B → A +foo3 : Π (A : Type) {B : Type}, A → B → A +foo4 : Π (A : Type) (B : Type), A → B → A +boo1 : Π {A : Type} {B : Type}, A → B → A +boo2 : Π {A : Type} (B : Type), A → B → A +boo3 : Π (A : Type) {B : Type}, A → B → A +boo4 : Π (A : Type) (B : Type), A → B → A param_binder_update.lean:70:12: error: invalid parameter binder type update, 'A' is a variable param_binder_update.lean:71:11: error: invalid variable binder type update, 'C' is not a variable param_binder_update.lean:72:12: error: invalid variable binder type update, 'C' is not a variable diff --git a/tests/lean/param_binder_update2.lean.expected.out b/tests/lean/param_binder_update2.lean.expected.out index 93052f0693..b5b750ee77 100644 --- a/tests/lean/param_binder_update2.lean.expected.out +++ b/tests/lean/param_binder_update2.lean.expected.out @@ -1,4 +1,4 @@ -foo1 : Π {A} {B}, A → B → A -foo2 : Π {A} B, A → B → A -foo3 : Π A {B}, A → B → A -foo4 : Π A B, A → B → A +foo1 : Π {A : Type} {B : Type}, A → B → A +foo2 : Π {A : Type} (B : Type), A → B → A +foo3 : Π (A : Type) {B : Type}, A → B → A +foo4 : Π (A : Type) (B : Type), A → B → A diff --git a/tests/lean/pattern_pp.lean.expected.out b/tests/lean/pattern_pp.lean.expected.out index 44952a01f8..6884cd4083 100644 --- a/tests/lean/pattern_pp.lean.expected.out +++ b/tests/lean/pattern_pp.lean.expected.out @@ -1,3 +1,3 @@ attribute [forward] definition Sum_weird : ∀ (f g h : ℕ → ℕ) (n : ℕ), Sum n (λ (x : ℕ), f (g (h x))) = 1 := -λ f g h n, sorry +λ (f g h : ℕ → ℕ) (n : ℕ), sorry diff --git a/tests/lean/pp.lean.expected.out b/tests/lean/pp.lean.expected.out index 43ae202ce6..be3384c8e0 100644 --- a/tests/lean/pp.lean.expected.out +++ b/tests/lean/pp.lean.expected.out @@ -1,7 +1,7 @@ -λ {A} B a b, a : Π {A} B, A → B → A -λ {A B} a b, a : Π {A B}, A → B → A -λ A {B} a b, a : Π A {B}, A → B → A -λ A B a b, a : Π A B, A → B → A -λ [A] B a b, a : Π [A] B, A → B → A -λ ⦃A⦄ {B} a b, a : Π ⦃A⦄ {B}, A → B → A -λ ⦃A B⦄ a b, a : Π ⦃A B⦄, A → B → A +λ {A : Type} (B : Type) (a : A) (b : B), a : Π {A : Type} (B : Type), A → B → A +λ {A B : Type} (a : A) (b : B), a : Π {A B : Type}, A → B → A +λ (A : Type) {B : Type} (a : A) (b : B), a : Π (A : Type) {B : Type}, A → B → A +λ (A B : Type) (a : A) (b : B), a : Π (A B : Type), A → B → A +λ [A : Type] (B : Type) (a : A) (b : B), a : Π [A : Type] (B : Type), A → B → A +λ ⦃A : Type⦄ {B : Type} (a : A) (b : B), a : Π ⦃A : Type⦄ {B : Type}, A → B → A +λ ⦃A B : Type⦄ (a : A) (b : B), a : Π ⦃A B : Type⦄, A → B → A diff --git a/tests/lean/pp_beta.lean.expected.out b/tests/lean/pp_beta.lean.expected.out index 5232dcad3d..e214e6af9a 100644 --- a/tests/lean/pp_beta.lean.expected.out +++ b/tests/lean/pp_beta.lean.expected.out @@ -1,2 +1,2 @@ 1 : ℕ -(λ x, x) 1 : ℕ +(λ (x : ℕ), x) 1 : ℕ diff --git a/tests/lean/pp_binder_types.lean.expected.out b/tests/lean/pp_binder_types.lean.expected.out index 4a816761f9..867d4e6ac0 100644 --- a/tests/lean/pp_binder_types.lean.expected.out +++ b/tests/lean/pp_binder_types.lean.expected.out @@ -1,4 +1,4 @@ definition f : Π (n : ℕ), n = n → ℕ → ℕ := -λ n H m, id (n + m) -definition f : Π (n : ℕ), n = n → ℕ → ℕ := +λ (n : ℕ) (H : n = n) (m : ℕ), id (n + m) +definition f : Π (n : ℕ), n = n → ℕ → ℕ := λ (n : ℕ) (H : n = n) (m : ℕ), id (n + m) diff --git a/tests/lean/ppbug.lean.expected.out b/tests/lean/ppbug.lean.expected.out index e69310943e..75eec5fa21 100644 --- a/tests/lean/ppbug.lean.expected.out +++ b/tests/lean/ppbug.lean.expected.out @@ -1 +1,2 @@ -list.rec_on : Π n, ?M_2 list.nil → (Π a a_1, ?M_2 a_1 → ?M_2 (a :: a_1)) → ?M_2 n +list.rec_on : + Π (n : list ?M_1), ?M_2 list.nil → (Π (a : ?M_1) (a_1 : list ?M_1), ?M_2 a_1 → ?M_2 (a :: a_1)) → ?M_2 n diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out index a811ee8a06..6825b973a5 100644 --- a/tests/lean/print_ax1.lean.expected.out +++ b/tests/lean/print_ax1.lean.expected.out @@ -1,3 +1,3 @@ -quot.sound : ∀ {A} [s] {a b}, a ≈ b → ⟦a⟧ = ⟦b⟧ -classical.strong_indefinite_description : Π {A} P, nonempty A → {x \ Exists P → P x} -propext : ∀ {a b}, (a ↔ b) → a = b +quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ +classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} +propext : ∀ {a b : Prop}, (a ↔ b) → a = b diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out index a811ee8a06..6825b973a5 100644 --- a/tests/lean/print_ax2.lean.expected.out +++ b/tests/lean/print_ax2.lean.expected.out @@ -1,3 +1,3 @@ -quot.sound : ∀ {A} [s] {a b}, a ≈ b → ⟦a⟧ = ⟦b⟧ -classical.strong_indefinite_description : Π {A} P, nonempty A → {x \ Exists P → P x} -propext : ∀ {a b}, (a ↔ b) → a = b +quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ +classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} +propext : ∀ {a b : Prop}, (a ↔ b) → a = b diff --git a/tests/lean/print_ax3.lean.expected.out b/tests/lean/print_ax3.lean.expected.out index 49be15964f..d05249b660 100644 --- a/tests/lean/print_ax3.lean.expected.out +++ b/tests/lean/print_ax3.lean.expected.out @@ -1,8 +1,8 @@ no axioms ------ -quot.sound : ∀ {A} [s] {a b}, a ≈ b → ⟦a⟧ = ⟦b⟧ -classical.strong_indefinite_description : Π {A} P, nonempty A → {x \ Exists P → P x} -propext : ∀ {a b}, (a ↔ b) → a = b +quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧ +classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A \ Exists P → P x} +propext : ∀ {a b : Prop}, (a ↔ b) → a = b ------ theorem foo3 : 0 = 0 := foo2 diff --git a/tests/lean/private_structure.lean.expected.out b/tests/lean/private_structure.lean.expected.out index 4ab4952d03..1e2c121f5c 100644 --- a/tests/lean/private_structure.lean.expected.out +++ b/tests/lean/private_structure.lean.expected.out @@ -1,10 +1,10 @@ bla : Type₁ point : Type₁ point.mk : ℕ → ℕ → point -point.rec : (Π x y, ?M_1 (point.mk x y)) → Π n, ?M_1 n -point.rec_on : Π n, (Π x y, ?M_1 (point.mk x y)) → ?M_1 n -point.cases_on : Π n, (Π x y, ?M_1 (point.mk x y)) → ?M_1 n -point.induction_on : ∀ n, (∀ x y, ?M_1 (point.mk x y)) → ?M_1 n +point.rec : (Π (x y : ℕ), ?M_1 (point.mk x y)) → Π (n : point), ?M_1 n +point.rec_on : Π (n : point), (Π (x y : ℕ), ?M_1 (point.mk x y)) → ?M_1 n +point.cases_on : Π (n : point), (Π (x y : ℕ), ?M_1 (point.mk x y)) → ?M_1 n +point.induction_on : ∀ (n : point), (∀ (x y : ℕ), ?M_1 (point.mk x y)) → ?M_1 n point.x : point → ℕ point.y : point → ℕ bla : Type₁ diff --git a/tests/lean/protected_test.lean.expected.out b/tests/lean/protected_test.lean.expected.out index a64fecefd2..9d307bb989 100644 --- a/tests/lean/protected_test.lean.expected.out +++ b/tests/lean/protected_test.lean.expected.out @@ -1,7 +1,7 @@ protected_test.lean:2:8: error: unknown identifier 'induction_on' protected_test.lean:3:8: error: unknown identifier 'rec_on' -nat.induction_on : ∀ n, ?M_1 0 → (∀ a, ?M_1 a → ?M_1 (succ a)) → ?M_1 n -le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b}, le ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 -le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b}, le ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 +nat.induction_on : ∀ (n : ℕ), ?M_1 0 → (∀ (a : ℕ), ?M_1 a → ?M_1 (succ a)) → ?M_1 n +le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, le ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 +le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, le ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 protected_test.lean:8:10: error: unknown identifier 'rec_on' -le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b}, le ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 +le.rec_on : le ?M_1 ?M_3 → ?M_2 ?M_1 → (∀ {b : ℕ}, le ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3 diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out index 4f1484d923..d925317acc 100644 --- a/tests/lean/quot_bug.lean.expected.out +++ b/tests/lean/quot_bug.lean.expected.out @@ -1 +1 @@ -λ x, f x +λ (x : A), f x diff --git a/tests/lean/rev_tac1.lean.expected.out b/tests/lean/rev_tac1.lean.expected.out index 262ccf2490..ea2efe2555 100644 --- a/tests/lean/rev_tac1.lean.expected.out +++ b/tests/lean/rev_tac1.lean.expected.out @@ -1,4 +1,4 @@ 3 b : ℕ, H : b > 0 -⊢ ∀ a, a > 0 → a > b → a = b → true +⊢ ∀ (a : ℕ), a > 0 → a > b → a = b → true diff --git a/tests/lean/sec_param_pp2.lean.expected.out b/tests/lean/sec_param_pp2.lean.expected.out index 2bb2b4e1d8..bf212bb403 100644 --- a/tests/lean/sec_param_pp2.lean.expected.out +++ b/tests/lean/sec_param_pp2.lean.expected.out @@ -1,4 +1,4 @@ id2 : (A → B → A) → A id2 : (A → B → A) → A id2 : ?M_1 → (A → ?M_1 → A) → A -id2 : ?M_1 → Π {B}, B → (?M_1 → B → ?M_1) → ?M_1 +id2 : ?M_1 → Π {B : Type}, B → (?M_1 → B → ?M_1) → ?M_1 diff --git a/tests/lean/simplifier_unsafe_nary.lean.expected.out b/tests/lean/simplifier_unsafe_nary.lean.expected.out index a3f0b1d52d..48b166e406 100644 --- a/tests/lean/simplifier_unsafe_nary.lean.expected.out +++ b/tests/lean/simplifier_unsafe_nary.lean.expected.out @@ -7,7 +7,7 @@ remark: set 'formatter.hide_full_terms' to false to see the complete term ?M_1 Unsafe version, should simplify and the proof should be incorrect simplifier_unsafe_nary.lean:17:0: error: type mismatch at application - (λ a a_1 e_1 a_2 a_3, congr (congr_arg eq e_1)) (op a (op b x y) z) (op a x (op a y z)) + (λ (a a_1 : A) (e_1 : a = a_1) (a_2 a_3 : A), congr (congr_arg eq e_1)) (op a (op b x y) z) (op a x (op a y z)) [flat (is_associative.op_assoc (op a)) (op a (op a x y) z = op a x (op a y z))] term [flat (is_associative.op_assoc (op a)) (op a (op a x y) z = op a x (op a y z))] diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out index 93c64e5833..8aa067301c 100644 --- a/tests/lean/struct_class.lean.expected.out +++ b/tests/lean/struct_class.lean.expected.out @@ -29,7 +29,7 @@ has_to_string : Type → Type has_to_tactic_format : Type → Type has_zero : Type → Type inhabited : Type → Type -is_associative : Π {A}, (A → A → A) → Type₁ +is_associative : Π {A : Type}, (A → A → A) → Type₁ monad : (Type → Type) → Type nonempty : Type → Prop point : Type → Type → Type @@ -66,7 +66,7 @@ has_to_string : Type → Type has_to_tactic_format : Type → Type has_zero : Type → Type inhabited : Type → Type -is_associative : Π {A}, (A → A → A) → Type₁ +is_associative : Π {A : Type}, (A → A → A) → Type₁ monad : (Type → Type) → Type nonempty : Type → Prop point : Type → Type → Type diff --git a/tests/lean/subpp.lean.expected.out b/tests/lean/subpp.lean.expected.out index 3e661d3108..28e6e568c9 100644 --- a/tests/lean/subpp.lean.expected.out +++ b/tests/lean/subpp.lean.expected.out @@ -1 +1 @@ -{x \ x > 0} : Type₁ +{x : ℕ \ x > 0} : Type₁ diff --git a/tests/lean/t11.lean.expected.out b/tests/lean/t11.lean.expected.out index f121ff9fd1..43663bc410 100644 --- a/tests/lean/t11.lean.expected.out +++ b/tests/lean/t11.lean.expected.out @@ -1,3 +1,3 @@ -∃ x, p x : bool -∃ x y, q x y : bool -λ x, x : A → A +∃ (x : A), p x : bool +∃ (x y : A), q x y : bool +λ (x : A), x : A → A diff --git a/tests/lean/t12.lean.expected.out b/tests/lean/t12.lean.expected.out index 3820611200..0d908e7008 100644 --- a/tests/lean/t12.lean.expected.out +++ b/tests/lean/t12.lean.expected.out @@ -1,2 +1,2 @@ -λ f g x y, f x (g x y) : (N → N → N) → (N → N → N) → N → N → N +λ (f g : N → N → N) (x y : N), f x (g x y) : (N → N → N) → (N → N → N) → N → N → N t12.lean:7:7: error: invalid expression diff --git a/tests/lean/t13.lean.expected.out b/tests/lean/t13.lean.expected.out index b7568be89d..5e0b935028 100644 --- a/tests/lean/t13.lean.expected.out +++ b/tests/lean/t13.lean.expected.out @@ -1,2 +1,2 @@ [choice g f] a b -λ h, h a b : (A → A → A) → A +λ (h : A → A → A), h a b : (A → A → A) → A diff --git a/tests/lean/univ_vars.lean.expected.out b/tests/lean/univ_vars.lean.expected.out index e1fb09b5cd..9c12fc3865 100644 --- a/tests/lean/univ_vars.lean.expected.out +++ b/tests/lean/univ_vars.lean.expected.out @@ -1,5 +1,5 @@ -id1 : Π A, A → A -id2.{l_2} : Π B, B → B -id3.{l_2} : Π C, C → C -foo.{l_2} : Π A₁ A₂, A₁ → A₂ → Prop +id1 : Π (A : Type.{u}), A → A +id2.{l_2} : Π (B : Type.{l_2}), B → B +id3.{l_2} : Π (C : Type.{l_2}), C → C +foo.{l_2} : Π (A₁ A₂ : Type.{l_2}), A₁ → A₂ → Prop Type.{m} : Type.{m+1} diff --git a/tests/lean/var2.lean.expected.out b/tests/lean/var2.lean.expected.out index fe5d06a76a..4983c8d570 100644 --- a/tests/lean/var2.lean.expected.out +++ b/tests/lean/var2.lean.expected.out @@ -1 +1 @@ -foo : Π B, B → Π A, A → A = B → Prop +foo : Π (B : Type), B → Π (A : Type), A → A = B → Prop diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out index 7e656c02d6..78ee85448c 100644 --- a/tests/lean/whnf.lean.expected.out +++ b/tests/lean/whnf.lean.expected.out @@ -1,4 +1,4 @@ -succ (nat.rec 2 (λ b₁ r, succ r) 0) +succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) 0) 3 -succ (nat.rec a (λ b₁ r, succ r) 0) +succ (nat.rec a (λ (b₁ r : ℕ), succ r) 0) succ a diff --git a/tests/lean/whnf_cache_bug.lean.expected.out b/tests/lean/whnf_cache_bug.lean.expected.out index 4bd645fcb6..ea56d2351a 100644 --- a/tests/lean/whnf_cache_bug.lean.expected.out +++ b/tests/lean/whnf_cache_bug.lean.expected.out @@ -1,2 +1,2 @@ ?m_1 -nat.succ (nat.rec 1 (λ b₁ r, nat.succ r) 0) +nat.succ (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0) diff --git a/tests/lean/whnf_core1.lean.expected.out b/tests/lean/whnf_core1.lean.expected.out index aa097db212..d9d7f1cdba 100644 --- a/tests/lean/whnf_core1.lean.expected.out +++ b/tests/lean/whnf_core1.lean.expected.out @@ -1,4 +1,4 @@ -nat.succ (nat.rec a (λ b₁ r, nat.succ r) (nat.rec 1 (λ b₁ r, nat.succ r) 0)) -nat.succ (nat.rec a (λ b₁ r, nat.succ r) (nat.rec 1 (λ b₁ r, nat.succ r) 0)) +nat.succ (nat.rec a (λ (b₁ r : ℕ), nat.succ r) (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0)) +nat.succ (nat.rec a (λ (b₁ r : ℕ), nat.succ r) (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0)) f a a + 2