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

chore(library/pp_options): pp.binder_types true by default

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-14 08:26:46 -07:00
parent 9bb8b0e6ef
commit cd6acb5d1d
53 changed files with 168 additions and 149 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/pp_options.cpp
View file

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

6
tests/lean/584a.lean.expected.out
View file

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

8
tests/lean/584b.lean.expected.out
View file

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

10
tests/lean/584c.lean.expected.out
View file

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

4
tests/lean/634d.lean.expected.out
View file

@ -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 : ℕ}, ℕ → ℕ

8
tests/lean/652.lean.expected.out
View file

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

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

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

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

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

15
tests/lean/acc_rec_bug.lean.expected.out
View file

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

36
tests/lean/anc1.lean.expected.out
View file

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

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

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

14
tests/lean/bug1.lean.expected.out
View file

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

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

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

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

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

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

@ -1 +1 @@
f : Π A, A → A
f : Π (A : Type), A → A

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

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

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

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

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

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

10
tests/lean/elab13.lean.expected.out
View file

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

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

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

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

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

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

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

8
tests/lean/hole_issue2.lean.expected.out
View file

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

17
tests/lean/let1.lean.expected.out
View file

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

8
tests/lean/nested1.lean.expected.out
View file

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

8
tests/lean/notation4.lean.expected.out
View file

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

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

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

20
tests/lean/param_binder_update.lean.expected.out
View file

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

8
tests/lean/param_binder_update2.lean.expected.out
View file

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

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

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

14
tests/lean/pp.lean.expected.out
View file

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

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

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

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

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

3
tests/lean/ppbug.lean.expected.out
View file

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

6
tests/lean/print_ax1.lean.expected.out
View file

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

6
tests/lean/print_ax2.lean.expected.out
View file

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

6
tests/lean/print_ax3.lean.expected.out
View file

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

8
tests/lean/private_structure.lean.expected.out
View file

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

8
tests/lean/protected_test.lean.expected.out
View file

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

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

@ -1 +1 @@
λ x, f x
λ (x : A), f x

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

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

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

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

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

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

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

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

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

@ -1 +1 @@
{x \ x > 0} : Type₁
{x : ℕ \ x > 0} : Type₁

6
tests/lean/t11.lean.expected.out
View file

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

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

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

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

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

8
tests/lean/univ_vars.lean.expected.out
View file

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

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

@ -1 +1 @@
foo : Π B, B → Π A, A → A = B → Prop
foo : Π (B : Type), B → Π (A : Type), A → A = B → Prop

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

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

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

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

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

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