chore: add workarounds

@Kha It seems the recent parser modifications created some unexpected
problems. I didn't investigate them. I am "lost" in the elaborator and
dependent pattern matching land.

1) We can't write anymore
```
f [1, 2, 3] |>.run' 0 = Except.ok ()
```
We have to use parentheses and the error message is weird :(
```
(f [1, 2, 3] |>.run' 0) = Except.ok ()
```

2) I had to add comments to `macro.lean`, I didn't find a workaround
for one of the rules. BTW, I had to add a bunch of `:term` for fixing
the other rules, and the error messages were counterintuitive.

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]

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

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

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 α] : α × α :=