From c3d62c107652215c13e3636d67e1bae5f039eeda Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Thu, 29 Jul 2021 15:41:53 -0700
Subject: [PATCH] chore: patch tests for pp.analyze default

---
 tests/lean/220.lean.expected.out              |  2 +-
 tests/lean/223.lean.expected.out              |  6 +--
 tests/lean/236.lean.expected.out              |  2 +-
 tests/lean/243.lean.expected.out              |  4 +-
 tests/lean/255.lean.expected.out              |  4 +-
 tests/lean/276.lean.expected.out              |  2 +-
 tests/lean/283.lean.expected.out              |  6 +--
 tests/lean/301.lean.expected.out              |  2 +-
 tests/lean/343.lean.expected.out              |  4 +-
 tests/lean/389.lean.expected.out              |  4 +-
 tests/lean/415.lean.expected.out              |  6 +--
 tests/lean/423.lean.expected.out              |  4 +-
 tests/lean/439.lean.expected.out              | 22 ++++----
 tests/lean/PPRoundtrip.lean.expected.out      | 25 ++++-----
 tests/lean/StxQuot.lean.expected.out          |  2 +-
 tests/lean/appParserIssue.lean.expected.out   | 10 ++--
 .../lean/autoBoundErrorMsg.lean.expected.out  |  4 +-
 .../autoBoundImplicits1.lean.expected.out     |  2 +-
 .../autoBoundImplicits2.lean.expected.out     |  4 +-
 tests/lean/autoPPExplicit.lean.expected.out   |  2 +-
 tests/lean/binderCacheIssue.lean.expected.out | 10 ++--
 .../lean/binderCacheIssue2.lean.expected.out  |  4 +-
 tests/lean/cacheIssue.lean.expected.out       |  2 +-
 tests/lean/doNotation1.lean.expected.out      |  2 +-
 .../lean/eagerCoeExpansion.lean.expected.out  | 21 +++-----
 tests/lean/elseifDoErrorPos.lean.expected.out |  2 +-
 tests/lean/emptyc.lean.expected.out           |  2 +-
 tests/lean/eta.lean.expected.out              |  6 +--
 tests/lean/evalWithMVar.lean.expected.out     |  8 +--
 tests/lean/funExpected.lean.expected.out      |  2 +-
 .../hidingInaccessibleNames.lean.expected.out |  6 +--
 tests/lean/holes.lean.expected.out            | 14 +++--
 tests/lean/inductive1.lean.expected.out       |  2 +-
 tests/lean/infoTree.lean.expected.out         | 37 ++++++-------
 .../interactive/completion2.lean.expected.out | 52 +++++++++++++------
 tests/lean/jason1.lean.expected.out           | 40 ++++++++++----
 .../lean/ll_infer_type_bug.lean.expected.out  |  6 +--
 tests/lean/macroPrio.lean.expected.out        |  4 +-
 tests/lean/macroResolveName.lean.expected.out |  4 +-
 tests/lean/match1.lean.expected.out           | 23 ++++----
 tests/lean/matchApp.lean.expected.out         |  3 +-
 tests/lean/matchunit.lean.expected.out        |  4 +-
 ...licitWithForwardNamedDep.lean.expected.out |  6 +--
 tests/lean/modBug.lean.expected.out           |  2 +-
 .../mulcommErrorMessage.lean.expected.out     |  8 +--
 tests/lean/namedHoles.lean.expected.out       |  6 +--
 tests/lean/parserPrio.lean.expected.out       |  6 +--
 tests/lean/ppExpr.lean.expected.out           |  4 +-
 tests/lean/ppMotives.lean.expected.out        | 37 +++++++------
 tests/lean/ppNotationCode.lean.expected.out   | 40 +++++++-------
 tests/lean/ppProofs.lean.expected.out         | 20 +++----
 tests/lean/ppite.lean.expected.out            |  4 +-
 tests/lean/pplevel.lean.expected.out          |  2 +-
 tests/lean/precissues.lean.expected.out       | 14 ++---
 tests/lean/rewrite.lean.expected.out          |  2 +-
 tests/lean/safeShadowing.lean.expected.out    | 14 ++---
 .../sanitizeMacroScopes.lean.expected.out     |  2 +-
 tests/lean/scopedunifhint.lean.expected.out   | 10 ++--
 .../simpArgTypeMismatch.lean.expected.out     |  2 +-
 tests/lean/structInstError.lean.expected.out  |  2 +-
 tests/lean/unhygienic.lean.expected.out       |  4 +-
 tests/lean/unifHintAndTC.lean.expected.out    |  2 +-
 62 files changed, 300 insertions(+), 258 deletions(-)

diff --git a/tests/lean/220.lean.expected.out b/tests/lean/220.lean.expected.out
index 8ca1c2420e..46e8bc8c28 100644
--- a/tests/lean/220.lean.expected.out
+++ b/tests/lean/220.lean.expected.out
@@ -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 => []
diff --git a/tests/lean/223.lean.expected.out b/tests/lean/223.lean.expected.out
index 9ba1868a58..dca5c16463 100644
--- a/tests/lean/223.lean.expected.out
+++ b/tests/lean/223.lean.expected.out
@@ -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 _
diff --git a/tests/lean/236.lean.expected.out b/tests/lean/236.lean.expected.out
index 226d08e3ac..4725b33322 100644
--- a/tests/lean/236.lean.expected.out
+++ b/tests/lean/236.lean.expected.out
@@ -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
diff --git a/tests/lean/243.lean.expected.out b/tests/lean/243.lean.expected.out
index a036080057..80d009511c 100644
--- a/tests/lean/243.lean.expected.out
+++ b/tests/lean/243.lean.expected.out
@@ -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
diff --git a/tests/lean/255.lean.expected.out b/tests/lean/255.lean.expected.out
index a854e5268a..1aa9bc4b5f 100644
--- a/tests/lean/255.lean.expected.out
+++ b/tests/lean/255.lean.expected.out
@@ -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
diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out
index ec3a1028b5..090cae994b 100644
--- a/tests/lean/276.lean.expected.out
+++ b/tests/lean/276.lean.expected.out
@@ -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
diff --git a/tests/lean/283.lean.expected.out b/tests/lean/283.lean.expected.out
index 2490e69737..fb37509315 100644
--- a/tests/lean/283.lean.expected.out
+++ b/tests/lean/283.lean.expected.out
@@ -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
diff --git a/tests/lean/301.lean.expected.out b/tests/lean/301.lean.expected.out
index 8fc4ec4b44..8fc6632c6c 100644
--- a/tests/lean/301.lean.expected.out
+++ b/tests/lean/301.lean.expected.out
@@ -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
diff --git a/tests/lean/343.lean.expected.out b/tests/lean/343.lean.expected.out
index 620d3337ad..5b2234ded5 100644
--- a/tests/lean/343.lean.expected.out
+++ b/tests/lean/343.lean.expected.out
@@ -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)}
diff --git a/tests/lean/389.lean.expected.out b/tests/lean/389.lean.expected.out
index ce7f012f50..030da157c4 100644
--- a/tests/lean/389.lean.expected.out
+++ b/tests/lean/389.lean.expected.out
@@ -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
diff --git a/tests/lean/415.lean.expected.out b/tests/lean/415.lean.expected.out
index 156d5d2966..89268ecdeb 100644
--- a/tests/lean/415.lean.expected.out
+++ b/tests/lean/415.lean.expected.out
@@ -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
diff --git a/tests/lean/423.lean.expected.out b/tests/lean/423.lean.expected.out
index 72f19f0263..2b08400483 100644
--- a/tests/lean/423.lean.expected.out
+++ b/tests/lean/423.lean.expected.out
@@ -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
diff --git a/tests/lean/439.lean.expected.out b/tests/lean/439.lean.expected.out
index d332ec7119..f2e2011d3c 100644
--- a/tests/lean/439.lean.expected.out
+++ b/tests/lean/439.lean.expected.out
@@ -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
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index 0e1333b7be..b5540ccd7d 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -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
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index a303f4dbcc..c85bad5038 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -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"
diff --git a/tests/lean/appParserIssue.lean.expected.out b/tests/lean/appParserIssue.lean.expected.out
index 70dc265afa..a3c322097a 100644
--- a/tests/lean/appParserIssue.lean.expected.out
+++ b/tests/lean/appParserIssue.lean.expected.out
@@ -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
diff --git a/tests/lean/autoBoundErrorMsg.lean.expected.out b/tests/lean/autoBoundErrorMsg.lean.expected.out
index 0c98635691..e9dd505072 100644
--- a/tests/lean/autoBoundErrorMsg.lean.expected.out
+++ b/tests/lean/autoBoundErrorMsg.lean.expected.out
@@ -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
diff --git a/tests/lean/autoBoundImplicits1.lean.expected.out b/tests/lean/autoBoundImplicits1.lean.expected.out
index 6892ceb092..2c984af1a6 100644
--- a/tests/lean/autoBoundImplicits1.lean.expected.out
+++ b/tests/lean/autoBoundImplicits1.lean.expected.out
@@ -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
diff --git a/tests/lean/autoBoundImplicits2.lean.expected.out b/tests/lean/autoBoundImplicits2.lean.expected.out
index 62c3b58d01..0733ef5d71 100644
--- a/tests/lean/autoBoundImplicits2.lean.expected.out
+++ b/tests/lean/autoBoundImplicits2.lean.expected.out
@@ -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
diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out
index 858b52c943..2cc5bfcdf1 100644
--- a/tests/lean/autoPPExplicit.lean.expected.out
+++ b/tests/lean/autoPPExplicit.lean.expected.out
@@ -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
diff --git a/tests/lean/binderCacheIssue.lean.expected.out b/tests/lean/binderCacheIssue.lean.expected.out
index 37e7de1b64..2c83ed4b51 100644
--- a/tests/lean/binderCacheIssue.lean.expected.out
+++ b/tests/lean/binderCacheIssue.lean.expected.out
@@ -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
diff --git a/tests/lean/binderCacheIssue2.lean.expected.out b/tests/lean/binderCacheIssue2.lean.expected.out
index d7ec2985b0..8275227ddc 100644
--- a/tests/lean/binderCacheIssue2.lean.expected.out
+++ b/tests/lean/binderCacheIssue2.lean.expected.out
@@ -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))
diff --git a/tests/lean/cacheIssue.lean.expected.out b/tests/lean/cacheIssue.lean.expected.out
index 9ac1aecd82..91a5b76b82 100644
--- a/tests/lean/cacheIssue.lean.expected.out
+++ b/tests/lean/cacheIssue.lean.expected.out
@@ -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
diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out
index 131fceda04..df33977254 100644
--- a/tests/lean/doNotation1.lean.expected.out
+++ b/tests/lean/doNotation1.lean.expected.out
@@ -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
diff --git a/tests/lean/eagerCoeExpansion.lean.expected.out b/tests/lean/eagerCoeExpansion.lean.expected.out
index 631b0802e7..fa0e2439ac 100644
--- a/tests/lean/eagerCoeExpansion.lean.expected.out
+++ b/tests/lean/eagerCoeExpansion.lean.expected.out
@@ -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
diff --git a/tests/lean/elseifDoErrorPos.lean.expected.out b/tests/lean/elseifDoErrorPos.lean.expected.out
index edd1b3b090..4bba58ef03 100644
--- a/tests/lean/elseifDoErrorPos.lean.expected.out
+++ b/tests/lean/elseifDoErrorPos.lean.expected.out
@@ -1,5 +1,5 @@
 elseifDoErrorPos.lean:4:7-7:14: error: application type mismatch
-  ite x
+  ite (α := IO Nat) x
 argument
   x
 has type
diff --git a/tests/lean/emptyc.lean.expected.out b/tests/lean/emptyc.lean.expected.out
index 3a730562fc..4ed6354e75 100644
--- a/tests/lean/emptyc.lean.expected.out
+++ b/tests/lean/emptyc.lean.expected.out
@@ -1,4 +1,4 @@
 emptyc.lean:19:0-19:2: error: ambiguous, possible interpretations 
   ∅
   
-  { x := 0 }
+  { x := 0 : A }
diff --git a/tests/lean/eta.lean.expected.out b/tests/lean/eta.lean.expected.out
index 18d1a8e46b..f15feb9a36 100644
--- a/tests/lean/eta.lean.expected.out
+++ b/tests/lean/eta.lean.expected.out
@@ -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
diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
index 388f412569..c998ca227e 100644
--- a/tests/lean/evalWithMVar.lean.expected.out
+++ b/tests/lean/evalWithMVar.lean.expected.out
@@ -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
diff --git a/tests/lean/funExpected.lean.expected.out b/tests/lean/funExpected.lean.expected.out
index e2cddfdc89..dc030ac87d 100644
--- a/tests/lean/funExpected.lean.expected.out
+++ b/tests/lean/funExpected.lean.expected.out
@@ -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
diff --git a/tests/lean/hidingInaccessibleNames.lean.expected.out b/tests/lean/hidingInaccessibleNames.lean.expected.out
index 263d3b8e50..3dcdf47ae8 100644
--- a/tests/lean/hidingInaccessibleNames.lean.expected.out
+++ b/tests/lean/hidingInaccessibleNames.lean.expected.out
@@ -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
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index ebdec58509..520bd3d0e3 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -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
diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out
index 9587a443b0..e0207ad06b 100644
--- a/tests/lean/inductive1.lean.expected.out
+++ b/tests/lean/inductive1.lean.expected.out
@@ -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'
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index 7df6659f5c..365fb4cfe8 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -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
diff --git a/tests/lean/interactive/completion2.lean.expected.out b/tests/lean/interactive/completion2.lean.expected.out
index 3a72228725..2f542e294f 100644
--- a/tests/lean/interactive/completion2.lean.expected.out
+++ b/tests/lean/interactive/completion2.lean.expected.out
@@ -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}
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
index 2af7ac48fb..9282ebb768 100644
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@@ -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
diff --git a/tests/lean/ll_infer_type_bug.lean.expected.out b/tests/lean/ll_infer_type_bug.lean.expected.out
index 3b9d50fca4..1a0f1177ff 100644
--- a/tests/lean/ll_infer_type_bug.lean.expected.out
+++ b/tests/lean/ll_infer_type_bug.lean.expected.out
@@ -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)
diff --git a/tests/lean/macroPrio.lean.expected.out b/tests/lean/macroPrio.lean.expected.out
index 3df230ae6d..e040e7cfb9 100644
--- a/tests/lean/macroPrio.lean.expected.out
+++ b/tests/lean/macroPrio.lean.expected.out
@@ -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
diff --git a/tests/lean/macroResolveName.lean.expected.out b/tests/lean/macroResolveName.lean.expected.out
index 93ebbc4d12..f403c23623 100644
--- a/tests/lean/macroResolveName.lean.expected.out
+++ b/tests/lean/macroResolveName.lean.expected.out
@@ -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)
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index 97a46ad3fa..240c0476b1 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -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
diff --git a/tests/lean/matchApp.lean.expected.out b/tests/lean/matchApp.lean.expected.out
index de40fb5583..77339294d1 100644
--- a/tests/lean/matchApp.lean.expected.out
+++ b/tests/lean/matchApp.lean.expected.out
@@ -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
diff --git a/tests/lean/matchunit.lean.expected.out b/tests/lean/matchunit.lean.expected.out
index 2ee74f1b1d..dffbcf2a1a 100644
--- a/tests/lean/matchunit.lean.expected.out
+++ b/tests/lean/matchunit.lean.expected.out
@@ -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
diff --git a/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out b/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out
index 12b80d2c1a..201f0e8edf 100644
--- a/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out
+++ b/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out
@@ -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
diff --git a/tests/lean/modBug.lean.expected.out b/tests/lean/modBug.lean.expected.out
index d23425f5f9..93891eccbb 100644
--- a/tests/lean/modBug.lean.expected.out
+++ b/tests/lean/modBug.lean.expected.out
@@ -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
diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out
index 8b3daf9bd3..82f5a0f814 100644
--- a/tests/lean/mulcommErrorMessage.lean.expected.out
+++ b/tests/lean/mulcommErrorMessage.lean.expected.out
@@ -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
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index 1882413c52..51a7904000 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/tests/lean/namedHoles.lean.expected.out
@@ -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
diff --git a/tests/lean/parserPrio.lean.expected.out b/tests/lean/parserPrio.lean.expected.out
index de146f7139..e0784fd6b1 100644
--- a/tests/lean/parserPrio.lean.expected.out
+++ b/tests/lean/parserPrio.lean.expected.out
@@ -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]
diff --git a/tests/lean/ppExpr.lean.expected.out b/tests/lean/ppExpr.lean.expected.out
index 0c21782097..7f766cd51f 100644
--- a/tests/lean/ppExpr.lean.expected.out
+++ b/tests/lean/ppExpr.lean.expected.out
@@ -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)
diff --git a/tests/lean/ppMotives.lean.expected.out b/tests/lean/ppMotives.lean.expected.out
index 53ae15e334..23595fc2b0 100644
--- a/tests/lean/ppMotives.lean.expected.out
+++ b/tests/lean/ppMotives.lean.expected.out
@@ -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
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index b6cf14899c..1e2fff5f05 100644
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@@ -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 ()
diff --git a/tests/lean/ppProofs.lean.expected.out b/tests/lean/ppProofs.lean.expected.out
index 3e0a00a1d7..ee0f6646f4 100644
--- a/tests/lean/ppProofs.lean.expected.out
+++ b/tests/lean/ppProofs.lean.expected.out
@@ -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
diff --git a/tests/lean/ppite.lean.expected.out b/tests/lean/ppite.lean.expected.out
index f15d4dfe23..b518e50304 100644
--- a/tests/lean/ppite.lean.expected.out
+++ b/tests/lean/ppite.lean.expected.out
@@ -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"
diff --git a/tests/lean/pplevel.lean.expected.out b/tests/lean/pplevel.lean.expected.out
index e6e05f6c2e..f6e5662cc1 100644
--- a/tests/lean/pplevel.lean.expected.out
+++ b/tests/lean/pplevel.lean.expected.out
@@ -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)
diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out
index 56b7e6d7ff..eaed8e3a7f 100644
--- a/tests/lean/precissues.lean.expected.out
+++ b/tests/lean/precissues.lean.expected.out
@@ -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
diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out
index c619e3c911..47a04c58e0 100644
--- a/tests/lean/rewrite.lean.expected.out
+++ b/tests/lean/rewrite.lean.expected.out
@@ -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)
diff --git a/tests/lean/safeShadowing.lean.expected.out b/tests/lean/safeShadowing.lean.expected.out
index 1df66ad3e0..a1ba09c982 100644
--- a/tests/lean/safeShadowing.lean.expected.out
+++ b/tests/lean/safeShadowing.lean.expected.out
@@ -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
diff --git a/tests/lean/sanitizeMacroScopes.lean.expected.out b/tests/lean/sanitizeMacroScopes.lean.expected.out
index a4a5799bc8..878f678fd2 100644
--- a/tests/lean/sanitizeMacroScopes.lean.expected.out
+++ b/tests/lean/sanitizeMacroScopes.lean.expected.out
@@ -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
diff --git a/tests/lean/scopedunifhint.lean.expected.out b/tests/lean/scopedunifhint.lean.expected.out
index 5b73b5eb90..11c8a9e959 100644
--- a/tests/lean/scopedunifhint.lean.expected.out
+++ b/tests/lean/scopedunifhint.lean.expected.out
@@ -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
diff --git a/tests/lean/simpArgTypeMismatch.lean.expected.out b/tests/lean/simpArgTypeMismatch.lean.expected.out
index dab7b20ba4..c60ad25f29 100644
--- a/tests/lean/simpArgTypeMismatch.lean.expected.out
+++ b/tests/lean/simpArgTypeMismatch.lean.expected.out
@@ -1,5 +1,5 @@
 simpArgTypeMismatch.lean:3:13-3:31: error: application type mismatch
-  decideEqFalse Unit
+  decideEqFalse (p := ?m) Unit
 argument
   Unit
 has type
diff --git a/tests/lean/structInstError.lean.expected.out b/tests/lean/structInstError.lean.expected.out
index 32fc54a551..cf099f6ede 100644
--- a/tests/lean/structInstError.lean.expected.out
+++ b/tests/lean/structInstError.lean.expected.out
@@ -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
diff --git a/tests/lean/unhygienic.lean.expected.out b/tests/lean/unhygienic.lean.expected.out
index d3f3aca4ef..97617f2e72 100644
--- a/tests/lean/unhygienic.lean.expected.out
+++ b/tests/lean/unhygienic.lean.expected.out
@@ -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
diff --git a/tests/lean/unifHintAndTC.lean.expected.out b/tests/lean/unifHintAndTC.lean.expected.out
index 81382ea1dd..e9201a8362 100644
--- a/tests/lean/unifHintAndTC.lean.expected.out
+++ b/tests/lean/unifHintAndTC.lean.expected.out
@@ -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