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

chore: patch tests for pp.analyze default

Browse source
This commit is contained in:
Daniel Selsam 2021-07-29 15:41:53 -07:00 • committed by Sebastian Ullrich
parent d28419594e
commit c3d62c1076
62 changed files with 300 additions and 258 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,5 +1,5 @@
def f : List Nat → List Nat :=
fun (x : List Nat) =>
fun x =>
match x with
| a :: xs@(b :: bs) => xs
| x => []

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

@ -1,8 +1,8 @@
def h.{u_1, u_2} : {α : Type u_1} → {β : Type u_2} → {f : α → β} → {b : β} → Imf f b → α :=
fun {α : Type u_1} {β : Type u_2} {f : α → β} (x : β) (x_1 : Imf f x) =>
fun {α} {β} {f} x x_1 =>
match x, x_1 with
| .(f a), Imf.mk a => a
theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a :=
fun (x x_1 : Sort u) (x_2 : x = x_1) (x_3 : x) =>
fun x x_1 x_2 x_3 =>
match x, x_1, x_2, x_3 with
| α, .(α), Eq.refl α, a => HEq.refl a
| α, .(α), Eq.refl α, a => HEq.refl _

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

@ -1,3 +1,3 @@
{ x := 10, b := true } : Foo
{ x := 10, b := true : Foo } : Foo
Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) Bool.true : Foo
{ x := OfNat.ofNat 10, b := Bool.true : Foo } : Foo

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

@ -1,5 +1,5 @@
243.lean:2:3-2:14: error: application type mismatch
{ fst := Bool, snd := true }
{ fst := Bool, snd := true : Sigma fun α => α }
argument
true
has type
@ -7,7 +7,7 @@ has type
but is expected to have type
Bool : Type
243.lean:13:3-13:8: error: application type mismatch
{ fst := A, snd := A.a }
{ fst := A, snd := A.a : Sigma fun α => α }
argument
A.a
has type

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

@ -1,6 +1,6 @@
id x : α
id x✝ : α
255.lean:16:7-16:8: error: unknown constant 'x✝'
id sorry : ?m
id (α := ?m) (sorryAx ?m : ?m) : ?m
255.lean:20:9-20:10: error: unknown constant 'x✝'
id sorry : ?m
id (α := ?m) (sorryAx ?m : ?m) : ?m

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

@ -1,2 +1,2 @@
fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → PEmpty.{u_1} → α
fun {α} => PEmpty.rec.{v, u_1} fun x => α : {α : Sort v} → PEmpty.{u_1} → α
276.lean:13:4-13:15: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion

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

@ -1,8 +1,8 @@
283.lean:1:22-1:25: error: application type mismatch
f (f ?m)
f (f (t := ?m) ?m : ?m)
argument
f ?m
f (t := ?m) ?m
has type
?m : Sort ?u
but is expected to have type
optParam (Sort ?u) t : Type ?u
optParam _ t : Type ?u

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

@ -3,7 +3,7 @@
301.lean:1:21-1:24: error: type mismatch
«»
(«»
fun (x : Nat) =>
fun x =>
match x with
| 0 => 0)
has type

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

@ -2,6 +2,8 @@
343.lean:30:24-30:54: error: stuck at solving universe constraint
max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
while trying to unify
Catish.Obj Catish.Obj
((Catish.Obj : Type (max ((max (?u + 1) (?u + 1)) + 1) ((max ?u ?u) + 1))) :
Type (max ((max (?u + 1) (?u + 1)) + 1) ((max ?u ?u) + 1)))
Catish.Obj
with
CatIsh.{max ?u ?u, max (?u + 1) (?u + 1)}

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

@ -1,9 +1,9 @@
389.lean:7:7-7:17: error: application type mismatch
getFoo bar
getFoo (A := ?m) bar
argument
bar
has type
Bar Nat : Type
but is expected to have type
Foo ?m : Sort (max 1 ?u)
Foo.{?u} ?m : Sort (max 1 ?u)
getFoo bar.toFoo : Nat

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

@ -1,4 +1,4 @@
Set.insert (Set.insert (Set.insert Set.empty 1) 2) 3 : Set Nat
fun (x y : Nat) => g { x := x, y := y } : Nat → Nat → Nat
fun (x y : Nat) => Set.insert (Set.insert Set.empty x) y : Nat → Nat → Set Nat
fun (x y : Nat) => { x := x, y := y } : Nat → Nat → Point
fun x y => g { x := x, y := y : Point } : Nat → Nat → Nat
fun x y => Set.insert (Set.insert Set.empty x) y : Nat → Nat → Set Nat
fun x y => { x := x, y := y : Point } : Nat → Nat → Point

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

@ -1,5 +1,5 @@
423.lean:3:35-3:40: error: application type mismatch
HAdd.hAdd a
HAdd.hAdd (α := Nat) a
argument
a
has type
@ -23,7 +23,7 @@ has type
but is expected to have type
Type ?u : Type (?u + 1)
423.lean:5:55-5:60: error: application type mismatch
HAdd.hAdd a
HAdd.hAdd (α := Nat) a
argument
a
has type

22
tests/lean/439.lean.expected.out
View file

@ -1,19 +1,19 @@
fn : {p : P} → Bar.fn p
439.lean:18:7-18:12: error: function expected at
Fn.imp fn ?m
439.lean:20:7-20:12: error: function expected at
Fn.imp.{imax u ?u} fn ?m
term has type
Bar.fn ?m
439.lean:29:7-29:11: error: function expected at
Fn.imp fn ?m
Bar.fn.{u, ?u} (P := P) ?m
439.lean:31:7-31:11: error: function expected at
Fn.imp.{imax u ?u} fn ?m
term has type
Bar.fn ?m
Fn.imp fn p : Bar.fn p
Fn.imp fn' p Bp : Bar.fn p
439.lean:39:7-39:12: error: application type mismatch
Fn.imp fn' ?m p
Bar.fn.{u, ?u} (P := P) ?m
Fn.imp.{imax u u_1} fn : Bar.fn p
Fn.imp.{imax u u_1} fn' Bp : Bar.fn p
439.lean:41:7-41:12: error: application type mismatch
Fn.imp.{imax u ?u} fn' ?m p
argument
p
has type
P : Sort u
but is expected to have type
Bar.fn ?m : Sort ?u
Bar.fn.{u, ?u} (P := P) ?m : Sort ?u

25
tests/lean/PPRoundtrip.lean.expected.out
View file

@ -11,21 +11,19 @@ List Nat
List.{0} Nat
id.{2} Nat
Sum.{0, 0} Nat Nat
id (@id Type Nat)
fun (a : Nat) => a
fun (a b : Nat) => a
fun (a : Nat)
(b : Bool) => a
fun {a b : Nat} => a
id (id Nat)
fun a => a
fun a b => a
fun a b => a
fun {a b} => a
typeAs
({α : Type} →
α → α)
fun {α : Type}
(a : α) => a
fun {α : Type}
fun {α} a => a
fun {α}
[inst :
ToString α]
(a : α) =>
a =>
@toString α inst a
(α : Type) → α
(α β : Type) → α
@ -41,7 +39,7 @@ Type → Type → Type
[inst :
ToString Nat],
x = x
∀ x, x = x
∀ (x : Nat), x = x
0
1
42
@ -53,10 +51,7 @@ Type → Type → Type
(1, 2).fst
decide (1 < 2) ||
true
id
(fun (a : Nat) =>
a)
0
id (fun a => a) 0
typeAs Nat
do
let x ← pure 1

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

@ -44,7 +44,7 @@ StxQuot.lean:18:15: error: expected term
"#[(numLit \"1\"), [(numLit \"2\") (numLit \"3\")], (numLit \"4\")]"
"#[(numLit \"2\")]"
StxQuot.lean:94:39-94:44: error: unexpected antiquotation splice
fun (a : ?m) => sorry : (a : ?m) → ?m a
fun a => sorryAx (?m a) : (a : ?m) → ?m a
"#[(some 1), (some 2)]"
StxQuot.lean:101:13-101:14: error: unknown identifier 'x' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
"`id._@.UnhygienicMain._hyg.1"

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

@ -1,5 +1,5 @@
f 1 fun (x : Nat) => x : Nat
f 1 fun (x : Nat) => x : Nat
f 1 fun (x : Nat) => x : Nat
f 1 fun (x : Nat) => x : Nat
f 1 fun (x : Nat) => x : Nat
f 1 fun x => x : Nat
f 1 fun x => x : Nat
f 1 fun x => x : Nat
f 1 fun x => x : Nat
f 1 fun x => x : Nat

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

@ -1,8 +1,8 @@
autoBoundErrorMsg.lean:1:34-1:39: error: don't know how to synthesize implicit argument
@Eq ?m a b
@Eq.{?u} (?m (α := α) : Sort ?u) a b
context:
α : Sort ?u
a b : ?m
a b : ?m (α := α)
h : ∀ {a b : α}, a = b
⊢ Sort ?u
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

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

@ -11,5 +11,5 @@ autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β'
autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n'
autoBoundImplicits1.lean:25:18-25:23: warning: declaration uses 'sorry'
f : {α : Type} → {n : Nat} → Vec α n → Vec α n
f mkVec : Vec ?m 0
f (α := ?m) (mkVec (α := ?m) : Vec ?m 0) : Vec ?m 0
f mkVec : Vec Nat 0

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

@ -1,5 +1,5 @@
g1 : ?m → ?m
g1 (α := ?m) : ?m → ?m
autoBoundImplicits2.lean:30:17-30:18: error: unknown universe level 'u'
autoBoundImplicits2.lean:33:17-33:18: error: unknown universe level 'β'
def h1.{u} : {m : Type u → Type u} → {α : Type u} → m α → m α :=
fun {m : Type u → Type u} {α : Type u} (a : m α) => a
fun {m} {α} a => a

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

@ -1,5 +1,5 @@
autoPPExplicit.lean:2:2-2:32: error: application type mismatch
@Eq.trans α a (b = c)
@Eq.trans.{?u} α a (b = c)
argument
b = c
has type

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

@ -1,4 +1,6 @@
LNot.unpackFun : LNot ?m → ∀ (p : ?m), ¬?m p
Funtype.unpack : LNot ?m → ∀ (p : ?m), ¬?m p
LNot.applyFun : LNot ?m → ∀ {p : ?m}, ¬?m p
Funtype.apply : LNot ?m → ∀ {p : ?m}, ¬?m p
LNot.unpackFun (P := ?m) (L := ?m) : LNot.{u_1} (P := ?m) ?m → ∀ (p : ?m), ¬?m p
Funtype.unpack (N := LNot.{u_1} (P := ?m) ?m) (O := ∀ (p : ?m), ¬?m p) (T :=
∀ {p : ?m}, ¬?m p) : LNot.{u_1} (P := ?m) ?m → ∀ (p : ?m), ¬?m p
LNot.applyFun (P := ?m) (L := ?m) : LNot.{u_1} (P := ?m) ?m → ∀ {p : ?m}, ¬?m p
Funtype.apply (N := LNot.{u_1} (P := ?m) ?m) (O := ∀ (p : ?m), ¬?m p) (T :=
∀ {p : ?m}, ¬?m p) : LNot.{u_1} (P := ?m) ?m → ∀ {p : ?m}, ¬?m p

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

@ -1,2 +1,2 @@
def foo.{u, u_1} : {P : Sort u} → Bar P → Type :=
fun {P : Sort u} (B : Bar P) => Foo ((p : P) → Bar.fn p) ({p : P} → Bar.fn p)
def foo.{u, u_1} : {P : Sort u} → Bar.{u, u_1} P → Type :=
fun {P} B => Foo.{imax u u_1} ((p : P) → (Bar.fn p : Sort u_1)) ({p : P} → (Bar.fn p : Sort u_1))

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

@ -1,3 +1,3 @@
foo Bool : Foo (Bool → Nat) ({p : Bool} → Nat)
foo _ : Foo (Bool → Nat) ({p : Bool} → Nat)
(foo Bool).f : Unit → Bool → Nat
(bar Bool).f : Unit → Bool → Nat

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

@ -21,7 +21,7 @@ doNotation1.lean:33:2-33:7: error: invalid 'do' element, it must be inside 'for'
doNotation1.lean:37:2-37:10: error: invalid 'do' element, it must be inside 'for'
doNotation1.lean:40:0-40:9: error: must be last element in a 'do' sequence
def f10 : Nat → IO Unit :=
fun (x : Nat) => IO.println x
fun x => IO.println x
doNotation1.lean:51:0-51:13: error: type mismatch
IO.mkRef true
has type

21
tests/lean/eagerCoeExpansion.lean.expected.out
View file

@ -1,25 +1,20 @@
def h : BV 32 → Array Bool :=
fun (x : BV 32) => (fun (x : BV 32) => g (f x).val) x
fun x => (fun (x : BV 32) => g (f x).val) x
def r : Nat → Prop :=
fun (a : Nat) => if a == 0 = true then a != 1 = true else a != 2 = true
fun a => if a == 0 = true then a != 1 = true else a != 2 = true
def r : Nat → Prop :=
fun (a : Nat) =>
fun a =>
@ite.{1} Prop
(@Eq.{1} Bool
(@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
(@BEq.beq.{0} Nat (@instBEq.{0} Nat fun a b => instDecidableEqNat a b) a
(@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
Bool.true)
(instDecidableEqBool
(@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
(@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
(instDecidableEqBool _ _)
(@Eq.{1} Bool
(@bne.{0} Nat (@instBEq.{0} Nat fun a b => instDecidableEqNat a b) a (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))
Bool.true)
(@Eq.{1} Bool
(@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
(@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))
Bool.true)
(@Eq.{1} Bool
(@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
(@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
(@bne.{0} Nat (@instBEq.{0} Nat fun a b => instDecidableEqNat a b) a (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
Bool.true)
def s : Option Nat :=
ConstantFunction.f myFun 3 <|> ConstantFunction.f myFun 4

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

@ -1,5 +1,5 @@
elseifDoErrorPos.lean:4:7-7:14: error: application type mismatch
ite x
ite (α := IO Nat) x
argument
x
has type

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

@ -1,4 +1,4 @@
emptyc.lean:19:0-19:2: error: ambiguous, possible interpretations
∅
{ x := 0 }
{ x := 0 : A }

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

@ -1,5 +1,5 @@
[Meta.debug] >> fun (x : Nat) => Nat.add
[Meta.debug] >> fun x => Nat.add
[Meta.debug] >> Nat.add
[Meta.debug] >> HAdd.hAdd 1
[Meta.debug] >> fun (x y z : Nat) => Nat.add z y
[Meta.debug] >> fun (y : Nat) => Nat.add y y
[Meta.debug] >> fun x y z => Nat.add z y
[Meta.debug] >> fun y => Nat.add y y

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

@ -1,11 +1,11 @@
Sum.someRight c : Option Nat
Sum.someRight.{u_1, 0} (α := ?m) (c (α := ?m) : Sum ?m Nat) : Option Nat
evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
@Sum.someRight ?m Nat c
@Sum.someRight.{?u, 0} ?m Nat (c (α := ?m) : Sum ?m Nat)
context:
⊢ Type ?u
evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
@c ?m
context:
⊢ Type ?u
Sum.someRight c : Option Nat
Sum.someRight c : Option Nat
Sum.someRight.{u_1, 0} (α := ?m) (c (α := ?m) : Sum ?m Nat) : Option Nat
Sum.someRight.{u_1, 0} (α := ?m) (c (α := ?m) : Sum ?m Nat) : Option Nat

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

@ -1,4 +1,4 @@
funExpected.lean:4:2-4:29: error: function expected at
List.map (fun (x : Nat) => x + 1) xs
List.map (β := ?m) (fun (x : Nat) => (HAdd.hAdd (β := ?m x) (γ := ?m) x 1 : ?m)) xs
term has type
List ?m

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

@ -8,7 +8,7 @@ a b : Nat
⊢ Nat
hidingInaccessibleNames.lean:2:16-2:17: error: don't know how to synthesize placeholder
context:
: [] ≠ []
: Ne (α := List Nat) [] []
⊢ Nat
hidingInaccessibleNames.lean:10:16-10:17: error: don't know how to synthesize placeholder
context:
@ -17,7 +17,7 @@ x✝⁴ : Nat
x✝³ : x✝⁵ ≠ []
x✝² : List Nat
x✝¹ : Nat
x✝ : x✝² ≠ []
x✝ : Ne (α := List Nat) x✝² []
⊢ Nat
hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
context:
@ -33,7 +33,7 @@ x✝⁴ : List Nat
x✝³ : Nat
x✝² : x✝⁴ ≠ []
x✝¹ : Nat
x✝ : [] ≠ []
x✝ : Ne (α := List Nat) [] []
⊢ Nat
case inl
p q : Prop

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

@ -3,12 +3,12 @@ holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
context:
case hole
x : Nat
y : Nat := g x + g x
y : Nat := g (β := ?m x) x + g (β := ?m x) x
⊢ Nat
holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
context:
x : Nat
y : Nat := g x + g x
y : Nat := g (β := ?m x) x + g (β := ?m x) x
⊢ Nat
holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
@g Nat (?m x) x
@ -23,11 +23,15 @@ x : Nat
holes.lean:13:8-13:11: error: failed to infer binder type
holes.lean:15:16-15:17: error: failed to infer binder type
holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
@f Nat (?m a) a
@f Nat
(?m _ :
let f : {α : Sort ?u} → {β : ?m a (α := α)} → α → α := fun {α} {β} a => a;
?m a (α := Nat))
a
context:
a : Nat
f : {α : Type} → {β : ?m a} → α → α := fun {α : Type} {β : ?m a} (a : α) => a
⊢ ?m a
f : {α : Type} → {β : ?m a (α := α)} → α → α := fun {α} {β} a => a
⊢ ?m a (α := Nat)
holes.lean:18:7-18:10: error: failed to infer binder type
holes.lean:21:25-22:4: error: failed to infer definition type
holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type

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

@ -24,7 +24,7 @@ inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and
inductive1.lean:100:0-100:4: error: constructor resulting type must be specified in inductive family declaration
inductive1.lean:105:7-105:9: error: type expected
failed to synthesize instance
CoeSort (Nat → Type) ?m
CoeSort.{2, ?u} (Nat → Type) ?m
inductive1.lean:108:0-108:10: error: unexpected constructor resulting type
Nat
inductive1.lean:118:7-118:11: error: unknown identifier 'cons'

37
tests/lean/infoTree.lean.expected.out
View file

@ -16,7 +16,7 @@
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.538} @ ⟨13, 24⟩-⟨13, 27⟩
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
let y : Nat × Nat := (x, x);
let y := (x, x);
id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabLetDecl
Nat × Nat : Type @ ⟨14, 6⟩†-⟨14, 7⟩† @ Lean.Elab.Term.elabHole
(x, x) : Nat × Nat @ ⟨14, 11⟩-⟨14, 17⟩ @ Lean.Elab.Term.elabAnonymousCtor
@ -74,9 +74,9 @@
0 : Nat @ ⟨17, 39⟩-⟨17, 40⟩ @ Lean.Elab.Term.elabNumLit
x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabIdent
x : Nat @ ⟨17, 43⟩-⟨17, 44⟩
fun (x y : Nat) (b : Bool) =>
fun x y b =>
ofEqTrue
(Eq.trans (congrFun (congrArg Eq (Nat.add_zero x)) x)
(Eq.trans (congrFun (β := fun a => Prop) (f := Eq (x + 0)) (g := Eq x) (congrArg Eq (Nat.add_zero x)) x)
(eqSelf x)) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨18, 2⟩-⟨19, 8⟩ @ Lean.Elab.Term.elabFun
Nat : Type @ ⟨18, 6⟩†-⟨18, 7⟩† @ Lean.Elab.Term.elabHole
x : Nat @ ⟨18, 6⟩-⟨18, 7⟩
@ -130,11 +130,11 @@
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.872} @ ⟨21, 36⟩-⟨21, 39⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
fun (x y : Nat) (b : Bool) =>
let x : Nat × Nat := (x + y, x - y);
fun x y b =>
let x := (x + y, x - y);
match x with
| (z, w) =>
let z1 : Nat := z + w;
let z1 := z + w;
z + z1 : Nat → Nat → Bool → Nat @ ⟨22, 2⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabFun
Nat : Type @ ⟨22, 6⟩†-⟨22, 7⟩† @ Lean.Elab.Term.elabHole
x : Nat @ ⟨22, 6⟩-⟨22, 7⟩
@ -142,10 +142,10 @@
y : Nat @ ⟨22, 8⟩-⟨22, 9⟩
Bool : Type @ ⟨22, 10⟩†-⟨22, 11⟩† @ Lean.Elab.Term.elabHole
b : Bool @ ⟨22, 10⟩-⟨22, 11⟩
let x : Nat × Nat := (x + y, x - y);
let x := (x + y, x - y);
match x with
| (z, w) =>
let z1 : Nat := z + w;
let z1 := z + w;
z + z1 : Nat @ ⟨23, 4⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl
Macro expansion
let (z, w) := (x + y, x - y)
@ -157,10 +157,10 @@
| (z, w) =>
let z1 := z + w
z + z1
let x : Nat × Nat := (x + y, x - y);
let x := (x + y, x - y);
match x with
| (z, w) =>
let z1 : Nat := z + w;
let z1 := z + w;
z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl
Nat × Nat : Type @ ⟨23, 8⟩†-⟨23, 14⟩† @ Lean.Elab.Term.elabHole
(x + y, x - y) : Nat × Nat @ ⟨23, 18⟩-⟨23, 32⟩ @ Lean.Elab.Term.expandParen
@ -193,7 +193,7 @@
x✝ : Nat × Nat @ ⟨23, 4⟩†-⟨25, 10⟩†
match x✝ with
| (z, w) =>
let z1 : Nat := z + w;
let z1 := z + w;
z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.elabMatch
Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
[.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩
@ -206,7 +206,7 @@
z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
w : Nat @ ⟨23, 12⟩-⟨23, 13⟩ @ Lean.Elab.Term.elabIdent
w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
let z1 : Nat := z + w;
let z1 := z + w;
z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl
Nat : Type @ ⟨24, 8⟩†-⟨24, 10⟩† @ Lean.Elab.Term.elabHole
z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ myMacro._@.Init.Notation._hyg.5829
@ -297,25 +297,26 @@
B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.1896} @ ⟨33, 19⟩-⟨33, 20⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
{ pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen
{ pair := ({ val := id : A }, { val := id : A }) :
B } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
({ val := id : A }, { val := id : A }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen
Macro expansion
({ val := id }, { val := id })
===>
Prod.mk✝ { val := id } { val := id }
({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩†-⟨34, 39⟩ @ Lean.Elab.Term.elabApp
({ val := id : A }, { val := id : A }) : A × A @ ⟨34, 10⟩†-⟨34, 39⟩ @ Lean.Elab.Term.elabApp
Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 40⟩†
{ val := id } : A @ ⟨34, 11⟩-⟨34, 24⟩ @ Lean.Elab.Term.StructInst.elabStructInst
{ val := id : A } : A @ ⟨34, 11⟩-⟨34, 24⟩ @ Lean.Elab.Term.StructInst.elabStructInst
id : Nat → Nat @ ⟨34, 20⟩-⟨34, 22⟩ @ Lean.Elab.Term.elabIdent
[.] `id : some Nat -> Nat @ ⟨34, 20⟩-⟨34, 22⟩
id : {α : Type} → α → α @ ⟨34, 20⟩-⟨34, 22⟩
val : Nat → Nat := id @ ⟨34, 13⟩-⟨34, 16⟩
{ val := id } : A @ ⟨34, 26⟩-⟨34, 39⟩ @ Lean.Elab.Term.StructInst.elabStructInst
{ val := id : A } : A @ ⟨34, 26⟩-⟨34, 39⟩ @ Lean.Elab.Term.StructInst.elabStructInst
id : Nat → Nat @ ⟨34, 35⟩-⟨34, 37⟩ @ Lean.Elab.Term.elabIdent
[.] `id : some Nat -> Nat @ ⟨34, 35⟩-⟨34, 37⟩
id : {α : Type} → α → α @ ⟨34, 35⟩-⟨34, 37⟩
val : Nat → Nat := id @ ⟨34, 28⟩-⟨34, 31⟩
pair : A × A := ({ val := id }, { val := id }) @ ⟨34, 2⟩-⟨34, 6⟩
pair : A × A := ({ val := id : A }, { val := id : A }) @ ⟨34, 2⟩-⟨34, 6⟩
def Nat.xor : Nat → Nat → Nat :=
bitwise bne
[Elab.info] command @ ⟨37, 0⟩-⟨38, 10⟩ @ Lean.Elab.Command.expandInCmd

52
tests/lean/interactive/completion2.lean.expected.out
View file

@ -1,31 +1,53 @@
{"textDocument": {"uri": "file://completion2.lean"},
"position": {"line": 19, "character": 10}}
{"items":
[{"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},
{"label": "ax1", "detail": "?a ≤ ?b → ?a - ?a ≤ ?b - ?b"},
{"label": "ex1", "detail": "?a ≤ ?b → ?a + ?a ≤ ?b + ?b"}],
[{"label": "ex2", "detail": "LE.le (α := Nat) ?a ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3",
"detail":
"LE.le (α := Nat) ?a ?b → LE.le (α := Nat) ?c ?d → HAdd.hAdd (α := Nat) ?a ?c ≤ HAdd.hAdd (α := Nat) ?b ?d"},
{"label": "ax1",
"detail":
"LE.le (α := Nat) ?a ?b → HSub.hSub (α := Nat) ?a ?a ≤ HSub.hSub (α := Nat) ?b ?b"},
{"label": "ex1",
"detail":
"LE.le (α := Nat) ?a ?b → HAdd.hAdd (α := Nat) ?a ?a ≤ HAdd.hAdd (α := Nat) ?b ?b"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completion2.lean"},
"position": {"line": 25, "character": 6}}
{"items":
[{"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},
{"label": "ax1", "detail": "?a ≤ ?b → ?a - ?a ≤ ?b - ?b"},
{"label": "ex1", "detail": "?a ≤ ?b → ?a + ?a ≤ ?b + ?b"}],
[{"label": "ex2", "detail": "LE.le (α := Nat) ?a ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3",
"detail":
"LE.le (α := Nat) ?a ?b → LE.le (α := Nat) ?c ?d → HAdd.hAdd (α := Nat) ?a ?c ≤ HAdd.hAdd (α := Nat) ?b ?d"},
{"label": "ax1",
"detail":
"LE.le (α := Nat) ?a ?b → HSub.hSub (α := Nat) ?a ?a ≤ HSub.hSub (α := Nat) ?b ?b"},
{"label": "ex1",
"detail":
"LE.le (α := Nat) ?a ?b → HAdd.hAdd (α := Nat) ?a ?a ≤ HAdd.hAdd (α := Nat) ?b ?b"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completion2.lean"},
"position": {"line": 30, "character": 21}}
{"items":
[{"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},
{"label": "ax1", "detail": "?a ≤ ?b → ?a - ?a ≤ ?b - ?b"},
{"label": "ex1", "detail": "?a ≤ ?b → ?a + ?a ≤ ?b + ?b"}],
[{"label": "ex2", "detail": "LE.le (α := Nat) ?a ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3",
"detail":
"LE.le (α := Nat) ?a ?b → LE.le (α := Nat) ?c ?d → HAdd.hAdd (α := Nat) ?a ?c ≤ HAdd.hAdd (α := Nat) ?b ?d"},
{"label": "ax1",
"detail":
"LE.le (α := Nat) ?a ?b → HSub.hSub (α := Nat) ?a ?a ≤ HSub.hSub (α := Nat) ?b ?b"},
{"label": "ex1",
"detail":
"LE.le (α := Nat) ?a ?b → HAdd.hAdd (α := Nat) ?a ?a ≤ HAdd.hAdd (α := Nat) ?b ?b"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completion2.lean"},
"position": {"line": 37, "character": 22}}
{"items":
[{"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},
{"label": "ex1", "detail": "?a ≤ ?b → ?a + ?a ≤ ?b + ?b"}],
[{"label": "ex2", "detail": "LE.le (α := Nat) ?a ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3",
"detail":
"LE.le (α := Nat) ?a ?b → LE.le (α := Nat) ?c ?d → HAdd.hAdd (α := Nat) ?a ?c ≤ HAdd.hAdd (α := Nat) ?b ?d"},
{"label": "ex1",
"detail":
"LE.le (α := Nat) ?a ?b → HAdd.hAdd (α := Nat) ?a ?a ≤ HAdd.hAdd (α := Nat) ?b ?b"}],
"isIncomplete": true}

40
tests/lean/jason1.lean.expected.out
View file

@ -3,23 +3,41 @@ jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))) :
EG
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))) :
EG
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
context:
G T Tm : Type
EG : G → G → Type
@ -38,7 +56,7 @@ jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
context:
G T Tm : Type
EG : G → G → Type
@ -57,7 +75,7 @@ jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
(?m G T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
context:
G T Tm : Type
EG : G → G → Type
@ -72,7 +90,7 @@ x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
@TySyntaxLayer.nat G T EG getCtx (?m _ T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
@ -87,7 +105,7 @@ x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
@TySyntaxLayer.nat G T EG getCtx (?m _ T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
@ -102,7 +120,7 @@ x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
@TySyntaxLayer.nat G T EG getCtx (?m _ T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
@ -117,7 +135,7 @@ x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
@TySyntaxLayer.top G T EG getCtx (?m _ T Tm EG ET ETm (@EGrfl) getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type

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

@ -1,6 +1,6 @@
unsafe def f._cstage2 : _obj → UInt8 :=
fun (x : _obj) =>
fun x =>
List.casesOn
fun (head tail : _obj) =>
let _x_1 : UInt8 := Nat.decLt 0 head;
fun head tail =>
let _x_1 := Nat.decLt 0 head;
Bool.casesOn false (f tail)

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

@ -1,6 +1,6 @@
0 + 1 : Nat
macroPrio.lean:12:7-12:13: error: ambiguous, possible interpretations
1 * 2
HMul.hMul (α := ?m) (β := ?m) (γ := ?m) 1 2
1 + 1
HAdd.hAdd (α := ?m) (β := ?m) (γ := ?m) 1 1
2 - 2 : Nat

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

@ -1,2 +1,4 @@
some `Lean.Macro : Option Name
[(`Nat.succ, [])] : List (Lean.Name × List ?m)
List.cons (α := Lean.Name × List ?m)
(Prod.mk (β := List ?m) `Nat.succ (List.nil (α := ?m) : List ?m) : Lean.Name × List ?m)
(List.nil (α := Lean.Name × List ?m) : List (Lean.Name × List ?m)) : List (Lean.Name × List ?m)

23
tests/lean/match1.lean.expected.out
View file

@ -21,31 +21,34 @@ constructor expected
[false, true, true]
match1.lean:136:7-136:22: error: invalid match-expression, type of pattern variable 'a' contains metavariables
?m
fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m
fun (x : Nat × Nat) =>
fun x => ?m x : Prod.{u_1, u_2} ?m ?m → ?m
fun x =>
match x with
| (a, b) => a + b : Nat × Nat → Nat
fun (x : Bool × Bool) =>
fun x =>
match x with
| (a, b) => a && b : Bool × Bool → Bool
fun (x : Nat × Nat) =>
fun x =>
match x with
| (a, b) => a + b : Nat × Nat → Nat
fun (x x_1 : Option Nat) =>
fun x x_1 =>
match x, x_1 with
| some a, some b => some (a + b)
| x, x_2 => none : Option Nat → Option Nat → Option Nat
fun (x : Nat) =>
fun x =>
(match x : Nat → Nat → Nat with
| 0 => id
| Nat.succ x => id)
x : Nat → Nat
fun (x : Array Nat) =>
fun x =>
match x with
| #[1, 2] => 2
| #[] => 0
| #[3, 4, 5] => 3
| x => 4 : Array Nat → Nat
g.match_1 : (motive : List ?m → Sort u_2) →
(x : List ?m) → ((a : ?m) → motive [a]) → ((x : List ?m) → motive x) → motive x
fun (e : Empty) => nomatch e : Empty → False
g.match_1 (α :=
?m) : (motive : List ?m → Sort u_2) →
(x : List ?m) →
((a : ?m) → motive (List.cons (α := ?m) a (List.nil (α := ?m) : List ?m) : List ?m)) →
((x : List ?m) → motive x) → motive x
fun e => nomatch e : Empty → False

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

@ -1,5 +1,4 @@
fun {α : Type} (motive : List α → List α → Type) (h1 : Unit → motive [] []) (h2 : (x : List α) → motive x [])
(h3 : (x x_1 : List α) → motive x x_1) =>
fun {α} motive h1 h2 h3 =>
match [], [] with
| [], [] => h1 ()
| x, [] => h2 x

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

@ -1,6 +1,6 @@
def f : Unit → Nat :=
fun (a : Unit) => 10
fun a => 10
def g : Unit → Unit :=
fun (a : Unit) =>
fun a =>
match a with
| b@PUnit.unit => b

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

@ -1,6 +1,6 @@
Foo.val : (α β : Type) → [self : Foo α β] → Nat
10
valOf2 Bool Bool : Nat
fun (x y : Nat) => f x y 10 : Nat → Nat → Nat
fun (a : Nat) => g a 10 : Nat → Nat
fun (a : Bool) => h Bool a true : Bool → Bool
fun x y => f x y 10 : Nat → Nat → Nat
fun a => g a 10 : Nat → Nat
fun a => h _ a true : Bool → Bool

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

@ -1,7 +1,7 @@
modBug.lean:1:32-1:62: error: application type mismatch
Nat.zeroNeOne (Nat.mod_zero 1)
argument
Nat.mod_zero 1
Nat.mod_zero _
has type
1 % 0 = 1 : Prop
but is expected to have type

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

@ -1,5 +1,5 @@
mulcommErrorMessage.lean:8:13-13:25: error: type mismatch
fun (a : ?m) (b : ?m a) => ?m a b
fun a b => ?m _ _
has type
(a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
but is expected to have type
@ -15,7 +15,7 @@ has type
but is expected to have type
true = false : Prop
mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
fun (a b : Bool) => Bool.casesOn a (?m a b) (?m a b)
fun a b => Bool.casesOn (motive := ?m a b) _ (?m _ _ : ?m a b false) (?m _ _ : ?m a b true)
has type
(a b : Bool) → ?m a b a : Sort (imax 1 1 ?u)
but is expected to have type
@ -25,9 +25,9 @@ the following variables have been introduced by the implicit lamda feature
b✝ : Bool
you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
mulcommErrorMessage.lean:16:12-17:47: error: application type mismatch
Bool.casesOn a ?m (Bool.casesOn b ?m ?m)
Bool.casesOn (motive := ?m a b) _ ?m (Bool.casesOn (motive := ?m a b) _ ?m ?m : ?m a b b)
argument
Bool.casesOn b ?m ?m
Bool.casesOn (motive := ?m a b) _ ?m ?m
has type
?m a b b : Sort ?u
but is expected to have type

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

@ -8,10 +8,10 @@ but is expected to have type
Bool : Type
g ?x ?x : Nat
20
foo (fun (x : Nat) => ?m x) ?hole : Nat
bla ?hole fun (x : Nat) => ?hole : Nat
foo (fun x => ?m x) ?hole : Nat
bla ?hole fun x => ?hole : Nat
namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
boo (fun (x : Nat) => ?m x) fun (y : Bool) => sorry : Nat
boo (fun x => ?m x) fun y => sorry : Nat
11
12
namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context

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

@ -1,7 +1,7 @@
[1, 2]
6
parserPrio.lean:26:7-26:10: error: ambiguous, possible interpretations
2 * 1
parserPrio.lean:28:7-28:10: error: ambiguous, possible interpretations
HMul.hMul (α := ?m) (β := ?m) (γ := ?m) 2 1
[1]
List.cons (α := ?m) 1 (List.nil (α := ?m) : List ?m)
[1, 2, 3]

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

@ -1,3 +1,3 @@
#0
fun (a : Prop) => a
id (@id Nat (id Nat.zero))
fun a => a
id (α := Nat) ((@id Nat (id (α := Nat) Nat.zero : Nat) : Nat) : Nat)

37
tests/lean/ppMotives.lean.expected.out
View file

@ -1,31 +1,30 @@
protected def Nat.add : Nat → Nat → Nat :=
fun (x x_1 : Nat) =>
Nat.brecOn x_1
(fun (x : Nat) (f : Nat.below x) (x_2 : Nat) =>
fun x x_1 =>
Nat.brecOn (motive := fun x => Nat → Nat) x_1
(fun x f x_2 =>
(match x_2, x with
| a, Nat.zero => fun (x : Nat.below Nat.zero) => a
| a, Nat.succ b => fun (x : Nat.below (Nat.succ b)) => Nat.succ (PProd.fst x.fst a))
| a, Nat.zero => fun x => a
| a, Nat.succ b => fun x => Nat.succ (PProd.fst x.fst a))
f)
x
protected def Nat.add : Nat → Nat → Nat :=
fun (x x_1 : Nat) =>
Nat.brecOn (motive := fun (x : Nat) => Nat → Nat) x_1
(fun (x : Nat) (f : Nat.below (motive := fun (x : Nat) => Nat → Nat) x) (x_2 : Nat) =>
(match x_2, x : (x x : Nat) → Nat.below (motive := fun (x : Nat) => Nat → Nat) x → Nat with
| a, Nat.zero => fun (x : Nat.below (motive := fun (x : Nat) => Nat → Nat) Nat.zero) => a
| a, Nat.succ b =>
fun (x : Nat.below (motive := fun (x : Nat) => Nat → Nat) (Nat.succ b)) => Nat.succ (PProd.fst x.fst a))
fun x x_1 =>
Nat.brecOn (motive := fun x => Nat → Nat) x_1
(fun x f x_2 =>
(match x_2, x : (x : Nat) → (x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat with
| a, Nat.zero => fun x => a
| a, Nat.succ b => fun x => Nat.succ (PProd.fst x.fst a))
f)
x
theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a :=
fun (x x_1 : Sort u) (x_2 : x = x_1) (x_3 : x) =>
fun x x_1 x_2 x_3 =>
match x, x_1, x_2, x_3 with
| α, .(α), Eq.refl α, a => HEq.refl a
| α, .(α), Eq.refl α, a => HEq.refl _
theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a :=
fun (x x_1 : Sort u) (x_2 : x = x_1) (x_3 : x) =>
match x, x_1, x_2, x_3 : ∀ (x x_4 : Sort u) (x_5 : x = x_4) (x_6 : x), cast x_5 x_6 ≅ x_6 with
| α, .(α), Eq.refl α, a => HEq.refl a
fun x x_1 x_2 x_3 =>
match x, x_1, x_2, x_3 : Sort u → Sort u → ∀ x_5, ∀ x_6, cast x_5 x_6 ≅ x_6 with
| α, .(α), Eq.refl α, a => HEq.refl _
def fact : Nat → Nat :=
fun (n : Nat) => Nat.recOn n 1 fun (n acc : Nat) => (n + 1) * acc
fun n => Nat.recOn (motive := fun n => Nat) n 1 fun n acc => (n + 1) * acc
def fact : Nat → Nat :=
fun (n : Nat) => Nat.recOn (motive := fun (n : Nat) => Nat) n 1 fun (n acc : Nat) => (n + 1) * acc
fun n => Nat.recOn (motive := fun n => Nat) n 1 fun n acc => (n + 1) * acc

40
tests/lean/ppNotationCode.lean.expected.out
View file

@ -2,14 +2,14 @@
Lean.ParserDescr.trailingNode `«term_+++_» 45 46
(Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46))
[Elab.definition.body] myMacro._@.ppNotationCode._hyg.21 : Lean.Macro :=
fun (x : Lean.Syntax) =>
let discr : Lean.Syntax := x;
fun x =>
let discr := x;
if Lean.Syntax.isOfKind discr `«term_+++_» = true then
let discr_1 : Lean.Syntax := Lean.Syntax.getArg discr 0;
let discr_2 : Lean.Syntax := Lean.Syntax.getArg discr 1;
let discr : Lean.Syntax := Lean.Syntax.getArg discr 2;
let rhs : Lean.Syntax := discr;
let lhs : Lean.Syntax := discr_1;
let discr_1 := Lean.Syntax.getArg discr 0;
let discr_2 := Lean.Syntax.getArg discr 1;
let discr := Lean.Syntax.getArg discr 2;
let rhs := discr;
let lhs := discr_1;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let scp ← Lean.getCurrMacroScope
@ -20,31 +20,31 @@ fun (x : Lean.Syntax) =>
[(`Nat.add, [])],
Lean.Syntax.node `null #[lhs, rhs]])
else
let discr : Lean.Syntax := x;
let discr := x;
throw Lean.Macro.Exception.unsupportedSyntax
[Elab.definition.body] unexpand._@.ppNotationCode._hyg.4 : Lean.PrettyPrinter.Unexpander :=
fun (x : Lean.Syntax) =>
let discr : Lean.Syntax := x;
fun x =>
let discr := x;
if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then
let discr_1 : Lean.Syntax := Lean.Syntax.getArg discr 0;
let discr_1 := Lean.Syntax.getArg discr 0;
cond (Lean.Syntax.isOfKind discr_1 `ident)
(let discr_2 : Lean.Syntax := Lean.Syntax.getArg discr 1;
(let discr_2 := Lean.Syntax.getArg discr 1;
if Lean.Syntax.matchesNull discr_2 2 = true then
let discr : Lean.Syntax := Lean.Syntax.getArg discr_2 0;
let discr_3 : Lean.Syntax := Lean.Syntax.getArg discr_2 1;
let rhs : Lean.Syntax := discr_3;
let lhs : Lean.Syntax := discr;
let discr := Lean.Syntax.getArg discr_2 0;
let discr_3 := Lean.Syntax.getArg discr_2 1;
let rhs := discr_3;
let lhs := discr;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure (Lean.Syntax.node `«term_+++_» #[lhs, Lean.Syntax.atom info "+++", rhs])
else
let discr : Lean.Syntax := Lean.Syntax.getArg discr 1;
let discr := Lean.Syntax.getArg discr 1;
throw ())
(let discr_2 : Lean.Syntax := Lean.Syntax.getArg discr 0;
let discr : Lean.Syntax := Lean.Syntax.getArg discr 1;
(let discr_2 := Lean.Syntax.getArg discr 0;
let discr := Lean.Syntax.getArg discr 1;
throw ())
else
let discr : Lean.Syntax := x;
let discr := x;
throw ()

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

@ -1,34 +1,34 @@
ppProofs.lean:1:47-1:48: error: don't know how to synthesize placeholder
ppProofs.lean:3:47-3:48: error: don't know how to synthesize placeholder
context:
α β : Sort u_1
b : β
a : α
h : α = β
⊢ h ▸ a = b
ppProofs.lean:2:50-2:51: error: don't know how to synthesize placeholder
ppProofs.lean:4:50-4:51: error: don't know how to synthesize placeholder
context:
α β : Sort u_1
b : β
a : α
h : α = β
⊢ (_ : α = β) ▸ a = b
ppProofs.lean:3:50-3:57: error: unsolved goals
ppProofs.lean:5:50-5:57: error: unsolved goals
α β : Sort ?u
b : β
a : α
h : α = β
⊢ (_ : α = β) ▸ a = b
ppProofs.lean:5:50-5:51: error: don't know how to synthesize placeholder
context:
α β : Sort u_1
b : β
a : α
h : α = β
⊢ _ ▸ a = b
ppProofs.lean:7:50-7:51: error: don't know how to synthesize placeholder
context:
α β : Sort u_1
b : β
a : α
h : α = β
⊢ _ ▸ a = b
ppProofs.lean:9:50-9:51: error: don't know how to synthesize placeholder
context:
α β : Sort u_1
b : β
a : α
h : α = β
⊢ id h ▸ a = b

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

@ -1,7 +1,7 @@
def f : List Nat → IO Unit :=
fun (xs : List Nat) =>
fun xs =>
List.forM xs
fun (x : Nat) =>
fun x =>
if x == 0 = true then
do
IO.println "foo"

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

@ -1,6 +1,6 @@
Type (max u v w) : Type ((max u v w) + 1)
Type u : Type (u + 1)
id.{max u v w} : {α : Sort (max u v w)} → α → α
@id.{max u v w} : {α : Sort (max u v w)} → α → α
Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max ((max u v) + 1) (w + 1))
Type (max (u + 1) w (v + 2)) : Type ((max (u + 1) w (v + 2)) + 1)
Type u_1 : Type (u_1 + 1)

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

@ -1,17 +1,17 @@
id fun (x : ?m) => x : ?m → ?m
id (α := ?m → ?m) fun (x : ?m) => x : ?m → ?m
0 : Nat
f 1 fun (x : Nat) => x : Nat
f 1 fun x => x : Nat
0 : Nat
f 1 fun (x : Nat) => x : Nat
id : ?m → ?m
f 1 fun x => x : Nat
id (α := ?m) : ?m → ?m
precissues.lean:15:10: error: expected command
id : ?m → ?m
id (α := ?m) : ?m → ?m
precissues.lean:17:10: error: expected command
1 : Nat
id ((fun (this : True) => this) True.intro) : True
0 = (fun (this : Nat) => this) 1 : Prop
0 =
let x : Nat := 0;
let x := 0;
x : Prop
p ↔ ¬q : Prop
True = ¬False : Prop
@ -22,5 +22,5 @@ p ∧ ¬q : Prop
¬p = q : Prop
id ¬p : Prop
∀ (a a : Nat), a = a : Prop
id : ?m → ?m
id (α := ?m) : ?m → ?m
precissues.lean:41:10: error: expected command

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

@ -2,7 +2,7 @@
as bs : List α
⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
rewrite.lean:12:20-12:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
List.reverse (List.reverse ?as)
List.reverse (α := ?m) (List.reverse (α := ?m) ?as : List ?m)
α : Type u_1
as bs : List α
⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)

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

@ -1,15 +1,15 @@
fun (a : α) => a : α → α
fun {α : Sort u_1} (a : α) => a : {α : Sort u_1} → α → α
fun (x x : Nat) => x : Nat → Nat → Nat
fun a => a : α → α
fun {α} a => a : {α : Sort u_1} → α → α
fun x x => x : Nat → Nat → Nat
def f : Nat → Nat → Nat :=
fun (x x : Nat) =>
fun x x =>
match x with
| 0 => x + 1
| Nat.succ x_1 => x + 2
fun {α_1 : Sort u_1} (a : α_1) => a : {α_1 : Sort u_1} → α_1 → α_1
fun (x x_1 : Nat) => x_1 : Nat → Nat → Nat
fun {α_1} a => a : {α_1 : Sort u_1} → α_1 → α_1
fun x x_1 => x_1 : Nat → Nat → Nat
def f : Nat → Nat → Nat :=
fun (x x_1 : Nat) =>
fun x x_1 =>
match x_1 with
| 0 => x_1 + 1
| Nat.succ x_2 => x_1 + 2

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

@ -1,4 +1,4 @@
fun (x : ?m) (x_1 : ?m x) => x : (x : ?m) → ?m x → ?m
fun x x_1 => x : (x : ?m) → ?m x → ?m
[Elab.step] expected type: <not-available>, term
fun x => m x
[Elab.step] expected type: Sort ?u, term

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

@ -1,5 +1,5 @@
scopedunifhint.lean:28:7-28:14: error: application type mismatch
mul ?m x
mul (s := ?m) ?m x
argument
x
has type
@ -7,7 +7,7 @@ has type
but is expected to have type
?m.α : Type ?u
scopedunifhint.lean:29:7-29:24: error: application type mismatch
mul ?m (x, x)
mul (s := ?m) ?m (x, x)
argument
(x, x)
has type
@ -15,7 +15,7 @@ has type
but is expected to have type
?m.α : Type ?u
scopedunifhint.lean:33:7-33:10: error: application type mismatch
?m*x
mul (s := ?m) ?m x
argument
x
has type
@ -25,7 +25,7 @@ but is expected to have type
x*x : Nat.Magma.α
x*x : Nat.Magma.α
scopedunifhint.lean:39:7-39:24: error: application type mismatch
?m*(x, x)
mul (s := ?m) ?m (x, x)
argument
(x, x)
has type
@ -34,7 +34,7 @@ but is expected to have type
?m.α : Type ?u
(x, x)*(x, x) : (Prod.Magma Nat.Magma Nat.Magma).α
scopedunifhint.lean:56:7-56:22: error: application type mismatch
?m*(x, x)
mul (s := ?m) ?m (x, x)
argument
(x, x)
has type

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

@ -1,5 +1,5 @@
simpArgTypeMismatch.lean:3:13-3:31: error: application type mismatch
decideEqFalse Unit
decideEqFalse (p := ?m) Unit
argument
Unit
has type

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

@ -1,2 +1,2 @@
structInstError.lean:5:7-5:29: error: invalid {...} notation, expected type is not known
{ x := 10, b := true } : Foo
{ x := 10, b := true : Foo } : Foo

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

@ -1,3 +1,3 @@
x : Bool
fun (x : Nat) => x : Nat → Nat
fun (x : Int) (x_1 : Nat) => x : Int → Nat → Int
fun x => x : Nat → Nat
fun x x_1 => x : Int → Nat → Int

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

@ -2,4 +2,4 @@
(100, 400)
(49, 576, 576)
def g : Int → Int → Int :=
fun (x y : Int) => @mul.{0} (@magmaOfMul.{0} Int Int.instMulInt) x y
fun x y => @mul.{0} (@magmaOfMul.{0} Int Int.instMulInt) x y