chore: make sure term and tactic parsers have disjoint infix operators

src/Init/Notation.lean

@@ -161,21 +161,16 @@ macro_rules
       `(%[ $elems,* | List.nil ])
 
 namespace Parser.Tactic
-/- The precedence 3 will "terminate" terms by
-   '<|>' (precedence 2) and '>>' (precedence 1). It should be used for any (potentially)
-   trailing expression parameters in the tactic DSL. -/
-def tacTerm : ParserDescr := ParserDescr.cat `term 3
-
 syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic
 syntax (name := intros) "intros " (colGt (ident <|> "_"))* : tactic
 syntax (name := revert) "revert " (colGt ident)+ : tactic
 syntax (name := clear) "clear " (colGt ident)+ : tactic
 syntax (name := subst) "subst " (colGt ident)+ : tactic
 syntax (name := assumption) "assumption" : tactic
-syntax (name := apply) "apply " tacTerm : tactic
-syntax (name := exact) "exact " tacTerm : tactic
-syntax (name := refine) "refine " tacTerm : tactic
-syntax (name := refine!) "refine! " tacTerm : tactic
+syntax (name := apply) "apply " term : tactic
+syntax (name := exact) "exact " term : tactic
+syntax (name := refine) "refine " term : tactic
+syntax (name := refine!) "refine! " term : tactic
 syntax (name := case) "case " ident " => " tacticSeq : tactic
 syntax (name := allGoals) "allGoals " tacticSeq : tactic
 syntax (name := focus) "focus " tacticSeq : tactic
@@ -187,9 +182,8 @@ syntax (name := generalize) "generalize " atomic(ident " : ")? term:51 " = " ide
 syntax (name := paren) "(" tacticSeq ")" : tactic
 syntax (name := withReducible) "withReducible " tacticSeq : tactic
 syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic
-syntax:2 (name := orelse) tactic "<|>" tactic:1 : tactic
-macro "try " t:tacticSeq : tactic => `(($t) <|> skip)
-
+syntax:2 (name := orelse) tactic "<or>" tactic:1 : tactic
+macro "try " t:tacticSeq : tactic => `($t <or> skip)
 macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; allGoals $y:tactic))
 
 macro "rfl" : tactic => `(exact rfl)
@@ -201,10 +195,10 @@ syntax locationTarget   := "⊢" <|> "|-"
 syntax locationHyp      := (colGt ident)+
 syntax location         := withPosition("at " locationWildcard <|> locationTarget <|> locationHyp)
 
-syntax (name := change) "change " tacTerm (location)? : tactic
-syntax (name := changeWith) "change " term " with " tacTerm (location)? : tactic
+syntax (name := change) "change " term (location)? : tactic
+syntax (name := changeWith) "change " term " with " term (location)? : tactic
 
-syntax rwRule    := ("←" <|> "<-")? tacTerm
+syntax rwRule    := ("←" <|> "<-")? term
 syntax rwRuleSeq := "[" rwRule,+,? "]"
 
 syntax (name := rewrite) "rewrite " rwRule (location)? : tactic
@@ -236,29 +230,29 @@ def expandERw : Macro :=
 def expandERwSeq : Macro :=
   fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite"))
 
-syntax (name := injection) "injection " tacTerm (" with " (colGt (ident <|> "_"))+)? : tactic
+syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
 
 syntax (name := «have») "have " haveDecl : tactic
 syntax (name := «suffices») "suffices " sufficesDecl : tactic
-syntax (name := «show») "show " tacTerm : tactic
+syntax (name := «show») "show " term : tactic
 syntax (name := «let») "let " letDecl : tactic
 syntax (name := «let!») "let! " letDecl : tactic
 syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
 
 syntax inductionAlt  := "| " (ident <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
 syntax inductionAlts := "with " withPosition( (colGe inductionAlt)+)
-syntax (name := induction) "induction " tacTerm,+ (" using " ident)?  ("generalizing " ident+)? (inductionAlts)? : tactic
-syntax casesTarget := atomic(ident " : ")? tacTerm
+syntax (name := induction) "induction " term,+ (" using " ident)?  ("generalizing " ident+)? (inductionAlts)? : tactic
+syntax casesTarget := atomic(ident " : ")? term
 syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
 
-syntax (name := existsIntro) "exists " tacTerm : tactic
+syntax (name := existsIntro) "exists " term : tactic
 
 /- We use a priority > default, to avoid ambiguity with the builtin `have` notation -/
-macro (priority := high) "have" x:ident " := " p:tacTerm : tactic => `(have $x:ident : _ := $p)
+macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
 
 syntax "repeat " tacticSeq : tactic
 macro_rules
-  | `(tactic| repeat $seq) => `(tactic| (($seq); repeat $seq) <|> skip)
+  | `(tactic| repeat $seq) => `(tactic| (($seq); repeat $seq) <or> skip)
 
 end Parser.Tactic
 end Lean

src/Lean/Elab/Tactic/Basic.lean

@@ -453,8 +453,8 @@ private def findTag? (gs : List MVarId) (tag : Name) : TacticM (Option MVarId) :
 
 @[builtinTactic «orelse»] def evalOrelse : Tactic := fun stx =>
   match stx with
-  | `(tactic| $tac1 <|> $tac2) => evalTactic tac1 <|> evalTactic tac2
-  | _                          => throwUnsupportedSyntax
+  | `(tactic| $tac1 <or> $tac2) => evalTactic tac1 <|> evalTactic tac2
+  | _                           => throwUnsupportedSyntax
 
 builtin_initialize registerTraceClass `Elab.tactic
 

tests/lean/run/allGoals.lean

@@ -39,10 +39,10 @@ theorem Weekday.nextOfPrevious'' (d : Weekday) : previous (next d) = d ∧ next
   apply And.intro <;> cases d <;> rfl
 
 open Lean.Parser.Tactic in
-macro "rwd " x:tacTerm : tactic => `(rw $x:term; done)
+macro "rwd " x:term : tactic => `(rw $x:term; done)
 
 theorem ex (a b c : α) (h₁ : a = b) (h₂ : a = c) : b = a ∧ c = a := by
-  apply And.intro <;> rwd h₁ <|> rwd h₂
+  apply And.intro <;> try rwd h₁ <or> rwd h₂
 
 theorem idEq (a : α) : id a = a :=
   rfl

tests/lean/run/elab_cmd.lean

@@ -20,7 +20,7 @@ elab "#check2" b:term : command => do
 #check2 10
 
 elab "try" t:tactic : tactic => do
-  let t' ← `(tactic| $t <|> skip);
+  let t' ← `(tactic| $t <or> skip);
   Lean.Elab.Tactic.evalTactic t'
 
 theorem tst (x y z : Nat) : y = z → x = x → x = y → x = z :=

tests/lean/run/newfrontend1.lean

@@ -111,7 +111,7 @@ intros h1 _ h3
 traceState
 focus
   refine! Eq.trans ?pre ?post
-  (exact h1) <|> (exact y; exact h3; assumption)
+  (exact h1) <or> (exact y; exact h3; assumption)
 
 namespace Foo
   def Prod.mk := 1