diff --git a/tests/lean/run/exp.lean b/tests/lean/run/exp.lean
index 856ad0d38f..0749d96fee 100644
--- a/tests/lean/run/exp.lean
+++ b/tests/lean/run/exp.lean
@@ -14,7 +14,7 @@ def Expr.times : Nat → Expr → Expr
   | k, plus e₁ e₂ => plus (times k e₁) (times k e₂)
   | k, mul e₁ e₂  => mul (times k e₁) e₂
 
-theorem eval_times (k : Nat) (e : Expr) : e.times k |>.eval = k * e.eval := by
+theorem eval_times (k : Nat) (e : Expr) : (e.times k |>.eval) = k * e.eval := by
   induction e with simp [Expr.times, Expr.eval]
   | plus e₁ e₂ ih₁ ih₂ => simp [ih₁, ih₂, Nat.left_distrib]
   | mul  _ _ ih₁ ih₂   => simp [ih₁, Nat.mul_assoc]
diff --git a/tests/lean/run/forBodyResultTypeIssue.lean b/tests/lean/run/forBodyResultTypeIssue.lean
index 3db7553115..f04dfdabda 100644
--- a/tests/lean/run/forBodyResultTypeIssue.lean
+++ b/tests/lean/run/forBodyResultTypeIssue.lean
@@ -8,10 +8,10 @@ for x in xs do
 #eval f [1, 2, 3] |>.run' 0
 #eval f [1, 0, 3] |>.run' 0
 
-theorem ex1 : f [1, 2, 3] |>.run' 0 = Except.ok () :=
+theorem ex1 : (f [1, 2, 3] |>.run' 0) = Except.ok () :=
 rfl
 
-theorem ex2 : f [1, 0, 3] |>.run' 0 = Except.error "contains zero" :=
+theorem ex2 : (f [1, 0, 3] |>.run' 0) = Except.error "contains zero" :=
 rfl
 
 universes u
diff --git a/tests/lean/run/macro.lean b/tests/lean/run/macro.lean
index c4b69e4da6..dab202b0f2 100644
--- a/tests/lean/run/macro.lean
+++ b/tests/lean/run/macro.lean
@@ -1,5 +1,3 @@
-
-
 abbrev Set (α : Type) := α → Prop
 axiom setOf {α : Type} : (α → Prop) → Set α
 axiom mem {α : Type} : α → Set α → Prop
@@ -9,7 +7,7 @@ axiom Union {α : Type} : Set (Set α) → Set α
 syntax:100 term " ∈ " term:99 : term
 
 macro_rules
-| `($x ∈ $s) => `(mem $x $s)
+| `($x:term ∈ $s:term) => `(mem $x:term $s:term)
 
 declare_syntax_cat index
 
@@ -20,19 +18,19 @@ syntax ident ":" term : index
 syntax "{" index " | " term "}" : term
 
 macro_rules
-| `({$l:term ≤ $x:ident < $u | $p}) => `(setOf (fun $x:ident => $l ≤ $x:ident ∧ $x:ident < $u ∧ $p))
-| `({$x:ident : $t | $p}) => `(setOf (fun ($x:ident : $t) => $p))
-| `({$x:term ∈ $s | $p}) => `(setOf (fun $x => $x ∈ $s ∧ $p))
-| `({$x:term ≤ $e | $p}) => `(setOf (fun $x => $x ≤ $e ∧ $p))
-| `({$b:term      | $r}) => `(setOf (fun $b => $r))
+-- | `({ $l:term ≤ $x:ident < $u:term | $p:term }) => `(setOf (fun $x:ident => $l:term ≤ $x:ident ∧ $x:ident < $u:term ∧ $p:term))
+| `({ $x:ident : $t:term | $p:term }) => `(setOf (fun ($x:ident : $t:term) => $p:term))
+| `({ $x:term ∈ $s:term | $p:term }) => `(setOf (fun $x:term => $x:term ∈ $s:term ∧ $p:term))
+| `({ $x:term ≤ $e:term | $p:term }) => `(setOf (fun $x:term => $x:term ≤ $e:term ∧ $p:term))
+| `({ $b:term | $r:term}) => `(setOf (fun $b:term => $r:term))
 
-#check { 1 ≤ x < 10 | x ≠ 5 }
+-- #check { 1 ≤ x < 10 | x ≠ 5 }
 #check { f : Nat → Nat | f 1  > 0 }
 
 syntax "⋃ " term ", " term : term
 
 macro_rules
-| `(⋃ $b, $r) => `(Union {$b:term | $r})
+| `(⋃ $b:term, $r:term) => `(Union {$b:term | $r:term})
 
 #check ⋃ x,              x = x
 #check ⋃ (x : Set Unit), x = x
diff --git a/tests/lean/run/optParam.lean b/tests/lean/run/optParam.lean
index 818d3c2623..abcfa2dec1 100644
--- a/tests/lean/run/optParam.lean
+++ b/tests/lean/run/optParam.lean
@@ -4,7 +4,7 @@ def p (x : Nat := 0) : Nat × Nat :=
 theorem ex1 : p.1 = 0 :=
 rfl
 
-theorem ex2 : p (x := 1) |>.2 = 1 :=
+theorem ex2 : (p (x := 1) |>.2) = 1 :=
 rfl
 
 def c {α : Type} [Inhabited α] : α × α :=