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

feat: use signature pretty printer in #check id/#check @id

Browse source
This commit is contained in:
Sebastian Ullrich 2022-12-12 13:43:54 +01:00 • committed by Gabriel Ebner
parent 84de976111
commit eaafd36918
41 changed files with 160 additions and 155 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Lean/Elab/BuiltinCommand.lean
View file

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

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

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

2
tests/lean/1074a.lean.expected.out
View file

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

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

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

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

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

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

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

12
tests/lean/593.lean.expected.out
View file

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

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

@ -1,4 +1,4 @@
foo : ⦃u : Unit⦄ → Unit
foo ⦃u : Unit⦄ : Unit
foo : ⦃u : Unit⦄ → Unit
bla : Unit
fun {u} => bla : {u : Unit} → Unit

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@ -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 α :=

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

@ -1 +1 @@
@D.toC_1 : {α : Type} → [self : D α] → C α
D.toC_1 {α : Type} [self : D α] : C α

76
tests/lean/diamond6.lean.expected.out
View file

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

41
tests/lean/diamond7.lean.expected.out
View file

@ -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} α :=

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

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

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

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

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

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

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

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

13
tests/lean/namePatEqThm.lean.expected.out
View file

@ -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✝ = ([], [])

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

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

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

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

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

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

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

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

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

@ -1,2 +1,2 @@
Ex.double : Nat → Nat
Nat.double (x : Nat) : Nat
protectedAlias.lean:9:7-9:13: error: unknown identifier 'double'

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

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

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

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

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

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

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

@ -1,4 +1,4 @@
g : ?m → ?m
f : ⦃α : Type⦄ → α → α
f ⦃α : Type⦄ (a : α) : α
g 1 : Nat
f 1 : Nat

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

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

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

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

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

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

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

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

12
tests/lean/varBinderUpdate.lean.expected.out
View file

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