From eaafd3691818469aff8f7ef20e011a6899b75ef2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 12 Dec 2022 13:43:54 +0100 Subject: [PATCH] feat: use signature pretty printer in `#check id`/`#check @id` --- src/Lean/Elab/BuiltinCommand.lean | 16 +++- tests/lean/1026.lean.expected.out | 2 +- tests/lean/1074a.lean.expected.out | 2 +- tests/lean/1098.lean.expected.out | 2 +- tests/lean/1377.lean.expected.out | 2 +- tests/lean/440.lean.expected.out | 2 +- tests/lean/593.lean.expected.out | 12 +-- tests/lean/604.lean.expected.out | 2 +- tests/lean/951.lean.expected.out | 4 +- tests/lean/974.lean.expected.out | 10 +-- tests/lean/986.lean.expected.out | 8 +- tests/lean/LE.lean.expected.out | 2 +- .../autoBoundImplicits1.lean.expected.out | 2 +- ...toImplicitChainNameIssue.lean.expected.out | 2 +- tests/lean/autoIssue.lean.expected.out | 4 +- tests/lean/binrel_binop.lean.expected.out | 6 +- tests/lean/ctorUnivTooBig.lean.expected.out | 2 +- .../derivingRpcEncoding.lean.expected.out | 10 +-- tests/lean/diamond2.lean.expected.out | 4 +- tests/lean/diamond5.lean.expected.out | 2 +- tests/lean/diamond6.lean.expected.out | 76 +++++++++---------- tests/lean/diamond7.lean.expected.out | 41 +++++----- tests/lean/eqValue.lean.expected.out | 8 +- tests/lean/heapSort.lean.expected.out | 3 +- tests/lean/levelNGen.lean.expected.out | 6 +- ...licitWithForwardNamedDep.lean.expected.out | 2 +- tests/lean/namePatEqThm.lean.expected.out | 13 ++-- tests/lean/openExport.lean.expected.out | 20 ++--- tests/lean/openScoped.lean.expected.out | 2 +- tests/lean/private.lean.expected.out | 2 +- tests/lean/protected.lean.expected.out | 4 +- tests/lean/protectedAlias.lean.expected.out | 2 +- tests/lean/prvCtor.lean.expected.out | 2 +- tests/lean/root.lean.expected.out | 6 +- tests/lean/sizeof.lean.expected.out | 2 +- tests/lean/strictImplicit.lean.expected.out | 2 +- tests/lean/struct1.lean.expected.out | 4 +- tests/lean/structInst1.lean.expected.out | 4 +- tests/lean/structuralEqns.lean.expected.out | 2 +- .../lean/terminationFailure.lean.expected.out | 6 +- tests/lean/varBinderUpdate.lean.expected.out | 12 +-- 41 files changed, 160 insertions(+), 155 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 2cd04e5679..2c6a26cb07 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -10,6 +10,7 @@ import Lean.Elab.Eval import Lean.Elab.Command import Lean.Elab.Open import Lean.Elab.SetOption +import Lean.PrettyPrinter namespace Lean.Elab.Command @@ -238,8 +239,19 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := ignoreStuckTC) let e ← Term.levelMVarToParam (← instantiateMVars e) let type ← inferType e - unless e.isSyntheticSorry do - logInfoAt tk m!"{e} : {type}" + if e.isSyntheticSorry then + return + -- show signature for `#check id`/`#check @id` + match term with + | `($_:ident) | `(@$_:ident) => + if let .const c _ := e then + logInfoAt tk <| .ofPPFormat { pp := fun + | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c + | none => return f!"{c}" -- should never happen + } + return + | _ => pure () + logInfoAt tk m!"{e} : {type}" | _ => throwUnsupportedSyntax @[builtin_command_elab Lean.Parser.Command.check] def elabCheck : CommandElab := elabCheckCore (ignoreStuckTC := true) diff --git a/tests/lean/1026.lean.expected.out b/tests/lean/1026.lean.expected.out index 81bbc37cbb..95ab948769 100644 --- a/tests/lean/1026.lean.expected.out +++ b/tests/lean/1026.lean.expected.out @@ -1,7 +1,7 @@ 1026.lean:1:4-1:7: warning: declaration uses 'sorry' 1026.lean:10:2-10:12: warning: declaration uses 'sorry' 1026.lean:9:8-9:10: warning: declaration uses 'sorry' -foo._unfold : ∀ (n : Nat), +_root_.foo._unfold (n : Nat) : foo n = if n = 0 then 0 else diff --git a/tests/lean/1074a.lean.expected.out b/tests/lean/1074a.lean.expected.out index df31fbbbf5..2435b73342 100644 --- a/tests/lean/1074a.lean.expected.out +++ b/tests/lean/1074a.lean.expected.out @@ -1,4 +1,4 @@ -Brx.interp._eq_1 : ∀ (n z : Term) (H_2 : Brx (Term.id2 n z)), +_root_.Brx.interp._eq_1 (n z : Term) (H_2 : Brx (Term.id2 n z)) : Brx.interp H_2 = match (_ : True ∧ Brx z) with | (_ : True ∧ Brx z) => Brx.interp Hz diff --git a/tests/lean/1098.lean.expected.out b/tests/lean/1098.lean.expected.out index 85da7a2f4f..da25021afa 100644 --- a/tests/lean/1098.lean.expected.out +++ b/tests/lean/1098.lean.expected.out @@ -3,7 +3,7 @@ number of parameters: 2 constructors: R.intro : ∀ {α β γ γ' : Type u_1} {x₀ : γ} {y₀ : γ'} {f : γ → α → γ} {g : γ' → α → γ'} {out : γ → β} {out' : γ' → β}, R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' } -@R.intro : ∀ {α β γ γ' : Type u_1} {x₀ : γ} {y₀ : γ'} {f : γ → α → γ} {g : γ' → α → γ'} {out : γ → β} {out' : γ' → β}, +R.intro.{u_1} {α β γ γ' : Type u_1} {x₀ : γ} {y₀ : γ'} {f : γ → α → γ} {g : γ' → α → γ'} {out : γ → β} {out' : γ' → β} : R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' } inductive Ex2.R.{u_1} : {α β : Type u_1} → FoldImpl α β → FoldImpl α β → Prop number of parameters: 2 diff --git a/tests/lean/1377.lean.expected.out b/tests/lean/1377.lean.expected.out index b22940f237..b3ffd2cae8 100644 --- a/tests/lean/1377.lean.expected.out +++ b/tests/lean/1377.lean.expected.out @@ -1,2 +1,2 @@ 1377.lean:3:2-3:5: warning: declaration uses 'sorry' -foo.bar : Unit → {n : Nat} → Fin n → Fin n +foo.bar (x✝ : Unit) {n : Nat} (a✝ : Fin n) : Fin n diff --git a/tests/lean/440.lean.expected.out b/tests/lean/440.lean.expected.out index 20febf6cb4..1a38cbe2ef 100644 --- a/tests/lean/440.lean.expected.out +++ b/tests/lean/440.lean.expected.out @@ -5,5 +5,5 @@ context: context: x : Nat ⊢ Nat -f : Nat → Nat +f (x : Nat) : Nat 440.lean:11:0-11:9: error: cannot evaluate code because 'g' uses 'sorry' and/or contains errors diff --git a/tests/lean/593.lean.expected.out b/tests/lean/593.lean.expected.out index e2a8396f88..fdaa9b7591 100644 --- a/tests/lean/593.lean.expected.out +++ b/tests/lean/593.lean.expected.out @@ -1,8 +1,8 @@ -Foo.bar : Nat -bar : Nat -bar : Nat +Foo.Bar.bar : Nat +Foo.Bar.bar : Nat +Foo.Bar.bar : Nat 593.lean:21:7-21:10: error: unknown identifier 'boo' 593.lean:26:7-26:10: error: unknown identifier 'bar' -boo : Nat -Foo.bar : Nat -bar : Nat +Foo.boo : Nat +Foo.Bar.bar : Nat +Foo.Bar.bar : Nat diff --git a/tests/lean/604.lean.expected.out b/tests/lean/604.lean.expected.out index 0e86618089..0e7384100d 100644 --- a/tests/lean/604.lean.expected.out +++ b/tests/lean/604.lean.expected.out @@ -1,4 +1,4 @@ -foo : ⦃u : Unit⦄ → Unit +foo ⦃u : Unit⦄ : Unit foo : ⦃u : Unit⦄ → Unit bla : Unit fun {u} => bla : {u : Unit} → Unit diff --git a/tests/lean/951.lean.expected.out b/tests/lean/951.lean.expected.out index 62f2c8e85d..44c6d7ad24 100644 --- a/tests/lean/951.lean.expected.out +++ b/tests/lean/951.lean.expected.out @@ -1,2 +1,2 @@ -instDecidableLeThingAInstLEThingA : (t₁ t₂ : ThingA) → Decidable (t₁ ≤ t₂) -instDecidableLeThingBInstLEThingB : (t₁ t₂ : ThingB) → Decidable (t₁ ≤ t₂) +instDecidableLeThingAInstLEThingA (t₁ t₂ : ThingA) : Decidable (t₁ ≤ t₂) +instDecidableLeThingBInstLEThingB (t₁ t₂ : ThingB) : Decidable (t₁ ≤ t₂) diff --git a/tests/lean/974.lean.expected.out b/tests/lean/974.lean.expected.out index 97674a3ada..afdd4a876d 100644 --- a/tests/lean/974.lean.expected.out +++ b/tests/lean/974.lean.expected.out @@ -1,7 +1,7 @@ -Formula.count_quantifiers._eq_1 : ∀ (x : Nat) (f₁ f₂ : Formula x), +_root_.Formula.count_quantifiers._eq_1.{u_1} (x✝ : Nat) (f₁ f₂ : Formula x✝) : Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂ -Formula.count_quantifiers._eq_2 : ∀ (x : Nat) (f : Formula (x + 1)), +_root_.Formula.count_quantifiers._eq_2.{u_1} (x✝ : Nat) (f : Formula (x✝ + 1)) : Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1 -Formula.count_quantifiers._eq_3 : ∀ (x : Nat) (x_1 : Formula x), - (∀ (f₁ f₂ : Formula x), x_1 = Formula.imp f₁ f₂ → False) → - (∀ (f : Formula (x + 1)), x_1 = Formula.all f → False) → Formula.count_quantifiers x_1 = 0 +_root_.Formula.count_quantifiers._eq_3.{u_1} (x✝ : Nat) (x✝¹ : Formula x✝) + (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = Formula.imp f₁ f₂ → False) + (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = Formula.all f → False) : Formula.count_quantifiers x✝¹ = 0 diff --git a/tests/lean/986.lean.expected.out b/tests/lean/986.lean.expected.out index 526756ac16..97e0f9ba40 100644 --- a/tests/lean/986.lean.expected.out +++ b/tests/lean/986.lean.expected.out @@ -1,7 +1,7 @@ -@Array.insertionSort.swapLoop._eq_1 : ∀ {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < Array.size a), - Array.insertionSort.swapLoop lt a 0 h = a -@Array.insertionSort.swapLoop._eq_2 : ∀ {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat) - (h : Nat.succ j' < Array.size a), +_root_.Array.insertionSort.swapLoop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) + (h : 0 < Array.size a) : Array.insertionSort.swapLoop lt a 0 h = a +_root_.Array.insertionSort.swapLoop._eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat) + (h : Nat.succ j' < Array.size a) : Array.insertionSort.swapLoop lt a (Nat.succ j') h = let_fun h' := (_ : j' < Array.size a); if lt a[Nat.succ j'] a[j'] = true then diff --git a/tests/lean/LE.lean.expected.out b/tests/lean/LE.lean.expected.out index 4156950003..b1971c693f 100644 --- a/tests/lean/LE.lean.expected.out +++ b/tests/lean/LE.lean.expected.out @@ -1,4 +1,4 @@ -LE'.refl : ∀ (n : Nat), LE' n n +LE'.refl (n : Nat) : LE' n n inductive LE' : Nat → Nat → Prop number of parameters: 1 constructors: diff --git a/tests/lean/autoBoundImplicits1.lean.expected.out b/tests/lean/autoBoundImplicits1.lean.expected.out index 3432f83ab4..746bc0f04a 100644 --- a/tests/lean/autoBoundImplicits1.lean.expected.out +++ b/tests/lean/autoBoundImplicits1.lean.expected.out @@ -8,6 +8,6 @@ autoBoundImplicits1.lean:24:33-24:34: error: unknown identifier 'α' autoBoundImplicits1.lean:24:37-24:38: error: unknown identifier 'β' autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β' autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n' -@f : {α : Type} → {n : Nat} → Vec α n → Vec α n +f {α : Type} {n : Nat} (xs : Vec α n) : Vec α n f mkVec : Vec ?m 0 f mkVec : Vec Nat 0 diff --git a/tests/lean/autoImplicitChainNameIssue.lean.expected.out b/tests/lean/autoImplicitChainNameIssue.lean.expected.out index cd3a94fcd5..e68366ea75 100644 --- a/tests/lean/autoImplicitChainNameIssue.lean.expected.out +++ b/tests/lean/autoImplicitChainNameIssue.lean.expected.out @@ -3,4 +3,4 @@ case nil α✝ : Type u_1 as : List α✝ ⊢ Palindrome (List.reverse []) -@palindrome_reverse : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as) +palindrome_reverse.{u_1} {α✝ : Type u_1} {as : List α✝} (h : Palindrome as) : Palindrome (List.reverse as) diff --git a/tests/lean/autoIssue.lean.expected.out b/tests/lean/autoIssue.lean.expected.out index cec0f07287..015b043e24 100644 --- a/tests/lean/autoIssue.lean.expected.out +++ b/tests/lean/autoIssue.lean.expected.out @@ -1,11 +1,11 @@ -A.a' : ∀ (self : A), self.x = 1 +A.a' (self : A) : self.x = 1 z : A this : z.x = 1 ⊢ z.x = 1 z : A this : z.x = 1 ⊢ z.x = 1 -@A.rec : {motive : A → Sort u_1} → ((x : Nat) → (a' : x = 1) → motive (A.mk x)) → (t : A) → motive t +A.rec.{u} {motive : A → Sort u} (mk : (x : Nat) → (a' : x = 1) → motive (A.mk x)) (t : A) : motive t z : A x : Nat a' : x = 1 diff --git a/tests/lean/binrel_binop.lean.expected.out b/tests/lean/binrel_binop.lean.expected.out index 3f1020dba4..4504c759ca 100644 --- a/tests/lean/binrel_binop.lean.expected.out +++ b/tests/lean/binrel_binop.lean.expected.out @@ -1,6 +1,6 @@ binrel_binop.lean:1:8-1:11: warning: declaration uses 'sorry' -ex1 : ∀ (a : Int) (b c : Nat), a = Int.ofNat b - Int.ofNat c +ex1 (a : Int) (b c : Nat) : a = Int.ofNat b - Int.ofNat c binrel_binop.lean:5:8-5:11: warning: declaration uses 'sorry' -ex2 : ∀ (a : Int) (b c : Nat), a = Int.ofNat b - Int.ofNat c +ex2 (a : Int) (b c : Nat) : a = Int.ofNat b - Int.ofNat c binrel_binop.lean:9:8-9:11: warning: declaration uses 'sorry' -ex3 : ∀ (a : Int) (b c : Nat), a = Int.ofNat (b - c) +ex3 (a : Int) (b c : Nat) : a = Int.ofNat (b - c) diff --git a/tests/lean/ctorUnivTooBig.lean.expected.out b/tests/lean/ctorUnivTooBig.lean.expected.out index 0281650c96..314cb76cd6 100644 --- a/tests/lean/ctorUnivTooBig.lean.expected.out +++ b/tests/lean/ctorUnivTooBig.lean.expected.out @@ -16,7 +16,7 @@ at universe level max (u+1) (v+1) it must be smaller than or equal to the inductive datatype universe level u+1 -@Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member a (a :: as) +Ex1.Member.head.{u} {α : Type u} {a : α} {as : List α} : Member a (a :: as) ctorUnivTooBig.lean:35:2-35:27: error: invalid universe level in constructor 'Ex3.Member.head', parameter 'as' has type List α at universe level diff --git a/tests/lean/derivingRpcEncoding.lean.expected.out b/tests/lean/derivingRpcEncoding.lean.expected.out index df4e315384..19f47d9a02 100644 --- a/tests/lean/derivingRpcEncoding.lean.expected.out +++ b/tests/lean/derivingRpcEncoding.lean.expected.out @@ -6,7 +6,7 @@ instRpcEncodableBarTrans : RpcEncodable BarTrans ok: {"bar": {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}} instRpcEncodableBaz : RpcEncodable Baz ok: {"arr": []} -@instRpcEncodableFooGeneric : {α : Type} → [inst : RpcEncodable α] → RpcEncodable (FooGeneric α) +instRpcEncodableFooGeneric {α : Type} [inst✝ : RpcEncodable α] : RpcEncodable (FooGeneric α) ok: {"a": 0} ok: {"b": 42, "a": 3} instRpcEncodableBazInductive : RpcEncodable BazInductive @@ -14,14 +14,14 @@ ok: {"baz": {"arr": [{"fooRef": {"p": "0"}, "fooJson": {"s": ""}}, {"fooRef": {"p": "1"}, "fooJson": {"s": ""}}]}} -@instRpcEncodableFooInductive : {α : Type} → [inst : RpcEncodable α] → RpcEncodable (FooInductive α) +instRpcEncodableFooInductive {α : Type} [inst✝ : RpcEncodable α] : RpcEncodable (FooInductive α) ok: {"a": [{"baz": {"arr": []}}, {"p": "0"}]} ok: {"b": {"n": 42, "m": 0, "a": {"baz": {"arr": []}}}} ok: {"a": [{"baz": {"arr": []}}, [{"a": [{"baz": {"arr": []}}, []]}]]} -@instRpcEncodableFooParam : {n : Nat} → RpcEncodable (FooParam n) +instRpcEncodableFooParam {n : Nat} : RpcEncodable (FooParam n) ok: {"a": 42} -@instRpcEncodableUnused : {α : Type} → RpcEncodable (Unused α) +instRpcEncodableUnused {α : Type} : RpcEncodable (Unused α) ok: "a" -@instRpcEncodableUnusedStruct : {α : Type} → RpcEncodable (UnusedStruct α) +instRpcEncodableUnusedStruct {α : Type} : RpcEncodable (UnusedStruct α) ok: {} Except.error "no inductive constructor matched" diff --git a/tests/lean/diamond2.lean.expected.out b/tests/lean/diamond2.lean.expected.out index 73237e4196..043fee2dfc 100644 --- a/tests/lean/diamond2.lean.expected.out +++ b/tests/lean/diamond2.lean.expected.out @@ -1,5 +1,5 @@ -@Foo1.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → Foo1 α -@Foo2.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → α → α → Foo2 α +Foo1.mk {α : Type} (toBar : Bar (α → α)) (β : Type) (b : α → β) : Foo1 α +Foo2.mk {α : Type} (toBar : Bar (α → α)) (β : Type) (b : α → β) (x1 x2 : α) : Foo2 α @[reducible] def Foo2.toBar : {α : Type} → Foo2 α → Bar (α → α) := fun α self => self.1 @[reducible] def Foo2.toBoo2 : {α : Type} → Foo2 α → Boo2 α := diff --git a/tests/lean/diamond5.lean.expected.out b/tests/lean/diamond5.lean.expected.out index ed3861d384..57061a4aad 100644 --- a/tests/lean/diamond5.lean.expected.out +++ b/tests/lean/diamond5.lean.expected.out @@ -1 +1 @@ -@D.toC_1 : {α : Type} → [self : D α] → C α +D.toC_1 {α : Type} [self : D α] : C α diff --git a/tests/lean/diamond6.lean.expected.out b/tests/lean/diamond6.lean.expected.out index 512a3caf4a..43b66d2836 100644 --- a/tests/lean/diamond6.lean.expected.out +++ b/tests/lean/diamond6.lean.expected.out @@ -1,46 +1,44 @@ -@FooAC.mk : {α : Type} → - [toFooComm : FooComm α] → - [toMul : Mul.{0} α] → - (∀ (a b c : α), - @Eq.{1} α - (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) - (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a b) c) - (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a - (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) b c))) → - (∀ (a b c : α), - @Eq.{1} α - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) c) - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b c))) → - (∀ (a b : α), - @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) → - FooAC α +FooAC.mk {α : Type} [toFooComm : FooComm α] [toMul : Mul.{0} α] + (add_assoc : + ∀ (a b c : α), + @Eq.{1} α + (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) + (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a b) c) + (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a + (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) b c))) + (mul_assoc : + ∀ (a b c : α), + @Eq.{1} α + (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) c) + (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b c))) + (mul_comm : + ∀ (a b : α), + @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) + (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) : + FooAC α def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α := fun (α : Type) (self : FooAC α) => @FooAssoc.mk α (@FooComm.toFoo α (@FooAC.toFooComm α self)) (@FooAC.toMul α self) (@FooAC.add_assoc α self) (@FooAC.mul_assoc α self) -@FooAC'.mk : {α : Type} → - [toFooComm : FooComm α] → - [toMul : Mul.{0} α] → - (∀ (a b c : α), - @Eq.{1} α - (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) - (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a b) c) - (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a - (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) b c))) → - (∀ (a b c : α), - @Eq.{1} α - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) c) - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b c))) → - α → - (∀ (a b : α), - @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) - (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) → - FooAC' α +FooAC'.mk {α : Type} [toFooComm : FooComm α] [toMul : Mul.{0} α] + (add_assoc : + ∀ (a b c : α), + @Eq.{1} α + (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) + (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a b) c) + (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a + (@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) b c))) + (mul_assoc : + ∀ (a b c : α), + @Eq.{1} α + (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) c) + (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b c))) + (one : α) + (mul_comm : + ∀ (a b : α), + @Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) + (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) : + FooAC' α def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α := fun (α : Type) (self : FooAC' α) => @FooAssoc'.mk α diff --git a/tests/lean/diamond7.lean.expected.out b/tests/lean/diamond7.lean.expected.out index 01d740379d..1621b5efbb 100644 --- a/tests/lean/diamond7.lean.expected.out +++ b/tests/lean/diamond7.lean.expected.out @@ -1,33 +1,28 @@ -@CommMonoid.mk.{u_1} : {α : Type u_1} → - [toMonoid : Monoid.{u_1} α] → - (∀ (a b : α), - @Eq.{u_1 + 1} α - (@HMul.hMul.{u_1, u_1, u_1} α α α - (@instHMul.{u_1} α (@Semigroup.toMul.{u_1} α (@Monoid.toSemigroup.{u_1} α toMonoid))) a b) - (@HMul.hMul.{u_1, u_1, u_1} α α α - (@instHMul.{u_1} α (@Semigroup.toMul.{u_1} α (@Monoid.toSemigroup.{u_1} α toMonoid))) b a)) → - CommMonoid.{u_1} α +CommMonoid.mk.{u} {α : Type u} [toMonoid : Monoid.{u} α] + (mul_comm : + ∀ (a b : α), + @Eq.{u + 1} α + (@HMul.hMul.{u, u, u} α α α (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α toMonoid))) a b) + (@HMul.hMul.{u, u, u} α α α (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α toMonoid))) b + a)) : + CommMonoid.{u} α def CommMonoid.toCommSemigroup.{u} : {α : Type u} → [self : CommMonoid.{u} α] → CommSemigroup.{u} α := fun (α : Type u) (self : CommMonoid.{u} α) => @CommSemigroup.mk.{u} α (@Monoid.toSemigroup.{u} α (@CommMonoid.toMonoid.{u} α self)) (@CommMonoid.mul_comm.{u} α self) -@CommGroup.mk.{u_1} : {α : Type u_1} → - [toGroup : Group.{u_1} α] → - (∀ (a b : α), - @Eq.{u_1 + 1} α - (@HMul.hMul.{u_1, u_1, u_1} α α α - (@instHMul.{u_1} α - (@Semigroup.toMul.{u_1} α (@Monoid.toSemigroup.{u_1} α (@Group.toMonoid.{u_1} α toGroup)))) - a b) - (@HMul.hMul.{u_1, u_1, u_1} α α α - (@instHMul.{u_1} α - (@Semigroup.toMul.{u_1} α (@Monoid.toSemigroup.{u_1} α (@Group.toMonoid.{u_1} α toGroup)))) - b a)) → - CommGroup.{u_1} α +CommGroup.mk.{u} {α : Type u} [toGroup : Group.{u} α] + (mul_comm : + ∀ (a b : α), + @Eq.{u + 1} α + (@HMul.hMul.{u, u, u} α α α + (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α (@Group.toMonoid.{u} α toGroup)))) a b) + (@HMul.hMul.{u, u, u} α α α + (@instHMul.{u} α (@Semigroup.toMul.{u} α (@Monoid.toSemigroup.{u} α (@Group.toMonoid.{u} α toGroup)))) b a)) : + CommGroup.{u} α def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α := fun (α : Type u) (self : CommGroup.{u} α) => @CommMonoid.mk.{u} α (@Group.toMonoid.{u} α (@CommGroup.toGroup.{u} α self)) (@CommGroup.mul_comm.{u} α self) -@Field.mk : {α : Type u_1} → [toDivisionRing : DivisionRing α] → (∀ (a b : α), a * b = b * a) → Field α +Field.mk.{u} {α : Type u} [toDivisionRing : DivisionRing α] (mul_comm : ∀ (a b : α), a * b = b * a) : Field α def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α := fun (α : Type u) [self : Field.{u} α] => self.1 def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α := diff --git a/tests/lean/eqValue.lean.expected.out b/tests/lean/eqValue.lean.expected.out index 11cbe21c74..c470287f82 100644 --- a/tests/lean/eqValue.lean.expected.out +++ b/tests/lean/eqValue.lean.expected.out @@ -1,4 +1,4 @@ -f._eq_1 : f 0 = 1 -f._eq_2 : f 100 = 2 -f._eq_3 : f 1000 = 3 -f._eq_4 : ∀ (x_2 : Nat), (x_2 = 99 → False) → (x_2 = 999 → False) → f (Nat.succ x_2) = f x_2 +_root_.f._eq_1 : f 0 = 1 +_root_.f._eq_2 : f 100 = 2 +_root_.f._eq_3 : f 1000 = 3 +_root_.f._eq_4 (x_2 : Nat) (x_3 : x_2 = 99 → False) (x_4 : x_2 = 999 → False) : f (Nat.succ x_2) = f x_2 diff --git a/tests/lean/heapSort.lean.expected.out b/tests/lean/heapSort.lean.expected.out index 6d8ef35cd9..e5013f9768 100644 --- a/tests/lean/heapSort.lean.expected.out +++ b/tests/lean/heapSort.lean.expected.out @@ -4,7 +4,8 @@ heapSort.lean:43:4-43:10: warning: declaration uses 'sorry' heapSort.lean:58:4-58:13: warning: declaration uses 'sorry' heapSort.lean:58:4-58:13: warning: declaration uses 'sorry' heapSort.lean:102:4-102:13: warning: declaration uses 'sorry' -@Array.heapSort.loop._eq_1 : ∀ {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) (out : Array α), +_root_.Array.heapSort.loop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) + (out : Array α) : Array.heapSort.loop lt a out = match e : BinaryHeap.max a with | none => out diff --git a/tests/lean/levelNGen.lean.expected.out b/tests/lean/levelNGen.lean.expected.out index bc952cb9b7..743e0c5919 100644 --- a/tests/lean/levelNGen.lean.expected.out +++ b/tests/lean/levelNGen.lean.expected.out @@ -1,5 +1,5 @@ -@test1 : {α : Sort u_2} → α → Sort u_1 +test1.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1 levelNGen.lean:3:4-3:9: warning: declaration uses 'sorry' -@test2 : {α : Sort u_2} → α → Sort u_1 +test2.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1 levelNGen.lean:5:33-5:38: warning: declaration uses 'sorry' -@test3 : {α : Sort u_2} → α → Sort u_1 +test3.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1 diff --git a/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out b/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out index ce1860b862..b80d58fcc0 100644 --- a/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out +++ b/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out @@ -1,4 +1,4 @@ -Foo.val : (α β : Type) → [self : Foo α β] → Nat +Foo.val (α β : Type) [self : Foo α β] : Nat 10 valOf2 Bool Bool : Nat fun x y => f x y 10 : Nat → Nat → Nat diff --git a/tests/lean/namePatEqThm.lean.expected.out b/tests/lean/namePatEqThm.lean.expected.out index 6f54d88cbf..83708b129a 100644 --- a/tests/lean/namePatEqThm.lean.expected.out +++ b/tests/lean/namePatEqThm.lean.expected.out @@ -1,7 +1,6 @@ -iota._eq_1 : iota 0 = [] -iota._eq_2 : ∀ (n : Nat), iota (Nat.succ n) = Nat.succ n :: iota n -f._eq_1 : ∀ (x_1 y : Nat), f [x_1, y] = ([x_1, y], [y]) -f._eq_2 : ∀ (x_1 y : Nat) (zs : List Nat), (zs = [] → False) → f (x_1 :: y :: zs) = f zs -f._eq_3 : ∀ (x : List Nat), - (∀ (x_1 y : Nat), x = [x_1, y] → False) → - (∀ (x_1 y : Nat) (zs : List Nat), x = x_1 :: y :: zs → False) → f x = ([], []) +_root_.iota._eq_1 : iota 0 = [] +_root_.iota._eq_2 (n : Nat) : iota (Nat.succ n) = Nat.succ n :: iota n +_root_.f._eq_1 (x_1 y : Nat) : f [x_1, y] = ([x_1, y], [y]) +_root_.f._eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 :: y :: zs) = f zs +_root_.f._eq_3 (x✝ : List Nat) (x_2 : ∀ (x y : Nat), x✝ = [x, y] → False) + (x_3 : ∀ (x y : Nat) (zs : List Nat), x✝ = x :: y :: zs → False) : f x✝ = ([], []) diff --git a/tests/lean/openExport.lean.expected.out b/tests/lean/openExport.lean.expected.out index 3bdff125ad..298c8e9481 100644 --- a/tests/lean/openExport.lean.expected.out +++ b/tests/lean/openExport.lean.expected.out @@ -1,13 +1,13 @@ -x : Nat -y : Nat -B.x : Nat -B.x : Nat +A.x : Nat +B.y : Nat +A.x : Nat +A.x : Nat B.y : Nat openExport.lean:19:7-19:8: error: unknown identifier 'x' openExport.lean:20:7-20:8: error: unknown identifier 'y' -x : Nat -y : Nat -x : Nat -y : Nat -z : Nat -z : Nat +A.x : Nat +B.y : Nat +A.x : Nat +B.y : Nat +B.z : Nat +B.z : Nat diff --git a/tests/lean/openScoped.lean.expected.out b/tests/lean/openScoped.lean.expected.out index 0d2f678226..966271cb67 100644 --- a/tests/lean/openScoped.lean.expected.out +++ b/tests/lean/openScoped.lean.expected.out @@ -1,6 +1,6 @@ openScoped.lean:1:8-1:15: error: unknown identifier 'epsilon' openScoped.lean:4:2-4:24: error: failed to synthesize instance Decidable (f = g) -@epsilon : {α : Sort u_1} → [h : Nonempty α] → (α → Prop) → α +Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α openScoped.lean:15:8-15:15: error: unknown identifier 'epsilon' openScoped.lean:20:8-20:15: error: unknown identifier 'epsilon' diff --git a/tests/lean/private.lean.expected.out b/tests/lean/private.lean.expected.out index d64383117f..81c1e96388 100644 --- a/tests/lean/private.lean.expected.out +++ b/tests/lean/private.lean.expected.out @@ -1,7 +1,7 @@ Bla.foo == "world" : Bool private.lean:14:12-14:15: error: private declaration 'Bla.foo' has already been declared foo == 0 : Bool -Bla.foo : String +_root_.Bla.foo : String Boo.Bla.boo == "world" : Bool Boo.Bla.boo ++ "world" : String Boo.Bla.boo == "world" : Bool diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out index fd077858bf..76fa2adca3 100644 --- a/tests/lean/protected.lean.expected.out +++ b/tests/lean/protected.lean.expected.out @@ -1,8 +1,8 @@ protected.lean:10:7-10:8: error: unknown identifier 'x' Foo.x : Nat -Foo.y : Nat +Bla.Foo.y : Nat protected.lean:22:7-22:8: error: unknown identifier 'y' -z : Nat +Bla.Foo.z : Nat protected.lean:25:14-25:15: error: protected declarations must be in a namespace protected.lean:28:14-28:15: error: unknown identifier 'f' 8 diff --git a/tests/lean/protectedAlias.lean.expected.out b/tests/lean/protectedAlias.lean.expected.out index 81af85f7d8..20030271b3 100644 --- a/tests/lean/protectedAlias.lean.expected.out +++ b/tests/lean/protectedAlias.lean.expected.out @@ -1,2 +1,2 @@ -Ex.double : Nat → Nat +Nat.double (x : Nat) : Nat protectedAlias.lean:9:7-9:13: error: unknown identifier 'double' diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out index 76f48d8183..38ef8c5ae1 100644 --- a/tests/lean/prvCtor.lean.expected.out +++ b/tests/lean/prvCtor.lean.expected.out @@ -1,4 +1,4 @@ -a : Nat +_root_.a : Nat prvCtor.lean:21:7-21:8: error: unknown identifier 'a' prvCtor.lean:23:25-23:27: error: overloaded, errors diff --git a/tests/lean/root.lean.expected.out b/tests/lean/root.lean.expected.out index 9321a8b14d..1e37734f21 100644 --- a/tests/lean/root.lean.expected.out +++ b/tests/lean/root.lean.expected.out @@ -1,4 +1,4 @@ -Bla.f : Nat → Nat +Bla.f (x : Nat) : Nat root.lean:21:14-21:22: error: protected declarations must be in a namespace root.lean:29:4-29:10: error: invalid declaration name `_root_`, `_root_` is a prefix used to refer to the 'root' namespace root.lean:31:0-31:32: error: invalid namespace '_root_', '_root_' is a reserved namespace @@ -6,8 +6,8 @@ root.lean:33:0-33:34: error: invalid namespace 'f._root_', '_root_' is a reserve root.lean:35:14-35:22: error: protected declarations must be in a namespace root.lean:41:7-41:8: error: unknown identifier 'h' root.lean:43:7-43:8: error: unknown identifier 'f' -f : Nat → Nat -_private.root.0.prv : Nat -> Nat +Bla.f (x : Nat) : Nat +_root_.prv (x : Nat) : Nat root.lean:90:48-90:52: error: unsolved goals x : Nat ⊢ isEven (x + 1 + 1) = isEven x diff --git a/tests/lean/sizeof.lean.expected.out b/tests/lean/sizeof.lean.expected.out index 0a5dc9a442..b732b071d9 100644 --- a/tests/lean/sizeof.lean.expected.out +++ b/tests/lean/sizeof.lean.expected.out @@ -7,5 +7,5 @@ 308 310 11 -@InfTree.node.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (children : Nat → InfTree α), +InfTree.node.sizeOf_spec.{u} {α : Type u} [inst✝ : SizeOf α] (children : Nat → InfTree α) : sizeOf (InfTree.node children) = 1 diff --git a/tests/lean/strictImplicit.lean.expected.out b/tests/lean/strictImplicit.lean.expected.out index a8f0383ac9..de6fe0a879 100644 --- a/tests/lean/strictImplicit.lean.expected.out +++ b/tests/lean/strictImplicit.lean.expected.out @@ -1,4 +1,4 @@ g : ?m → ?m -f : ⦃α : Type⦄ → α → α +f ⦃α : Type⦄ (a : α) : α g 1 : Nat f 1 : Nat diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index 01c176cb33..24ee44c45d 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/tests/lean/struct1.lean.expected.out @@ -27,5 +27,5 @@ but is expected to have type struct1.lean:44:0-44:13: error: invalid 'private' constructor in a 'private' structure struct1.lean:47:0-47:15: error: invalid 'protected' constructor in a 'private' structure struct1.lean:50:0-50:19: error: invalid 'protected' field in a 'private' structure -S : Type -S.mk2 : Nat → S +_root_.S : Type +_root_.S.mk2 (x : Nat) : S diff --git a/tests/lean/structInst1.lean.expected.out b/tests/lean/structInst1.lean.expected.out index 6cd127f3e2..408bf2f8ac 100644 --- a/tests/lean/structInst1.lean.expected.out +++ b/tests/lean/structInst1.lean.expected.out @@ -1,3 +1,3 @@ structInst1.lean:12:11-12:19: error: field 'toA' has already been specified -f5 : C → A → C -f6 : C → A → A +f5 (c : C) (a : A) : C +f6 (c : C) (a : A) : A diff --git a/tests/lean/structuralEqns.lean.expected.out b/tests/lean/structuralEqns.lean.expected.out index 1d8325e920..9035a4fe86 100644 --- a/tests/lean/structuralEqns.lean.expected.out +++ b/tests/lean/structuralEqns.lean.expected.out @@ -1,5 +1,5 @@ (some _private.structuralEqns.0.foo._unfold) -foo._unfold : ∀ (xs ys zs : List Nat), +_root_.foo._unfold (xs ys zs : List Nat) : foo xs ys zs = match (xs, ys) with | (xs', ys') => diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out index 4668ef79f1..0319f93eaf 100644 --- a/tests/lean/terminationFailure.lean.expected.out +++ b/tests/lean/terminationFailure.lean.expected.out @@ -5,8 +5,8 @@ with errors structural recursion does not handle mutually recursive functions failed to prove termination, use `termination_by` to specify a well-founded relation -f : Nat → Nat -f.g : Nat → Nat +f (x : Nat) : Nat +f.g (a✝ : Nat) : Nat 1 2 terminationFailure.lean:20:4-20:5: error: fail to show termination for @@ -19,5 +19,5 @@ argument #1 was not used for structural recursion structural recursion cannot be used failed to prove termination, use `termination_by` to specify a well-founded relation -h : Nat → Foo +h (x : Nat) : Foo Foo.a diff --git a/tests/lean/varBinderUpdate.lean.expected.out b/tests/lean/varBinderUpdate.lean.expected.out index 29f63c1c90..e789dfabe9 100644 --- a/tests/lean/varBinderUpdate.lean.expected.out +++ b/tests/lean/varBinderUpdate.lean.expected.out @@ -1,14 +1,14 @@ f Nat 5 : Nat g 5 : Nat -f : (α : Type) → [inst : Add α] → α → α -@g : {α : Type} → α → α +Ex1.f (α : Type) [inst✝ : Add α] (a : α) : α +Ex1.g {α : Type} (b : α) : α f Nat 5 : Nat g 5 : Nat -f : (α : Type) → α → α -@g : {β : Type} → β → β +Ex2.f (α : Type) (a : α) : α +Ex2.g {β : Type} (b : β) : β varBinderUpdate.lean:25:10-25:11: error: redundant binder annotation update -g : (α : Type) → (α → α) → α → α -h : (α : Type) → {f : α → α} → α → α +Ex3.g (α : Type) (f : α → α) (a : α) : α +Ex3.h (α : Type) {f : α → α} (a : α) : α g Nat Bool 10 "hello" true : Nat × String × Bool varBinderUpdate.lean:51:10-51:11: error: cannot change the binder annotation of the previously declared local instance `i` varBinderUpdate.lean:59:10-59:11: error: cannot update binder annotation of variables with default values/tactics