feat: use unicode(...) in Init/Notation and elsewhere (#10384)

This PR makes notations such as `∨`, `∧`, `≤`, and `≥` pretty print using ASCII versions when `pp.unicode` is false. Continuation of #10373. Closes #1056. This will require followup with a stage0 update and removal of the ASCII-only `<=` and `>=` syntaxes from `Init.Notation`, for cleanup.
2026-03-17 18:34:06 +00:00 · 2026-03-09 15:17:32 -07:00
parent 670360681f
commit 71ff366211
9 changed files with 52 additions and 37 deletions
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -280,7 +280,7 @@ resulting in `t'`, which becomes the new target subgoal. -/
 syntax (name := convConvSeq) "conv" " => " convSeq : conv

 /-- `· conv` focuses on the main conv goal and tries to solve it using `s`. -/
-macro dot:patternIgnore("· " <|> ". ") s:convSeq : conv => `(conv| {%$dot ($s) })
+macro dot:unicode("· ", ". ") s:convSeq : conv => `(conv| {%$dot ($s) })


 /-- `fail_if_success t` fails if the tactic `t` succeeds. -/
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -177,7 +177,7 @@ syntax (name := next) "next " binderIdent* " => " grindSeq : grind
 `· grindSeq` focuses on the main `grind` goal and tries to solve it using the given
 sequence of `grind` tactics.
 -/
-macro dot:patternIgnore("· " <|> ". ") s:grindSeq : grind => `(grind| next%$dot =>%$dot $s:grindSeq )
+macro dot:unicode("· ", ". ") s:grindSeq : grind => `(grind| next%$dot =>%$dot $s:grindSeq )

 /--
 `any_goals tac` applies the tactic `tac` to every goal,
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -366,16 +366,19 @@ recommended_spelling "shiftLeft" for "<<<" in [HShiftLeft.hShiftLeft, «term_<<<
 recommended_spelling "shiftRight" for ">>>" in [HShiftRight.hShiftRight, «term_>>>_»]
 recommended_spelling "not" for "~~~" in [Complement.complement, «term~~~_»]

-- declare ASCII alternatives first so that the latter Unicode unexpander wins
-@[inherit_doc] infix:50 " <= " => LE.le
-@[inherit_doc] infix:50 " ≤ "  => LE.le
-@[inherit_doc] infix:50 " < "  => LT.lt
-@[inherit_doc] infix:50 " >= " => GE.ge
-@[inherit_doc] infix:50 " ≥ "  => GE.ge
-@[inherit_doc] infix:50 " > "  => GT.gt
-@[inherit_doc] infix:50 " = "  => Eq
-@[inherit_doc] infix:50 " == " => BEq.beq
-@[inherit_doc] infix:50 " ≍ "  => HEq
+-- TODO(kmill) remove these after stage0 update. There are builtin macros still using `«term_>=_»`
+@[inherit_doc] infix:50 (priority := low) " >= " => GE.ge
+@[inherit_doc] infix:50 (priority := low) " <= " => LE.le
+macro_rules | `($x >= $y)  => `(binrel% GE.ge $x $y)
+macro_rules | `($x <= $y)  => `(binrel% LE.le $x $y)
+
+@[inherit_doc] infix:50 unicode(" ≤ ", " <= ") => LE.le
+@[inherit_doc] infix:50 " < "                  => LT.lt
+@[inherit_doc] infix:50 unicode(" ≥ ", " >= ") => GE.ge
+@[inherit_doc] infix:50 " > "                  => GT.gt
+@[inherit_doc] infix:50 " = "                  => Eq
+@[inherit_doc] infix:50 " == "                 => BEq.beq
+@[inherit_doc] infix:50 " ≍ "                  => HEq

 /-!
  Remark: the infix commands above ensure a delaborator is generated for each relations.
@@ -383,39 +386,27 @@ recommended_spelling "not" for "~~~" in [Complement.complement, «term~~~_»]
  It has better support for applying coercions. For example, suppose we have `binrel% Eq n i` where `n : Nat` and
  `i : Int`. The default elaborator fails because we don't have a coercion from `Int` to `Nat`, but
  `binrel%` succeeds because it also tries a coercion from `Nat` to `Int` even when the nat occurs before the int. -/
-macro_rules | `($x <= $y) => `(binrel% LE.le $x $y)
 macro_rules | `($x ≤ $y)  => `(binrel% LE.le $x $y)
 macro_rules | `($x < $y)  => `(binrel% LT.lt $x $y)
 macro_rules | `($x > $y)  => `(binrel% GT.gt $x $y)
-macro_rules | `($x >= $y) => `(binrel% GE.ge $x $y)
 macro_rules | `($x ≥ $y)  => `(binrel% GE.ge $x $y)
 macro_rules | `($x = $y)  => `(binrel% Eq $x $y)
 macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)

 recommended_spelling "le" for "≤" in [LE.le, «term_≤_»]
-/-- prefer `≤` over `<=` -/
-recommended_spelling "le" for "<=" in [LE.le, «term_<=_»]
 recommended_spelling "lt" for "<" in [LT.lt, «term_<_»]
 recommended_spelling "gt" for ">" in [GT.gt, «term_>_»]
 recommended_spelling "ge" for "≥" in [GE.ge, «term_≥_»]
-/-- prefer `≥` over `>=` -/
-recommended_spelling "ge" for ">=" in [GE.ge, «term_>=_»]
 recommended_spelling "eq" for "=" in [Eq, «term_=_»]
 recommended_spelling "beq" for "==" in [BEq.beq, «term_==_»]
 recommended_spelling "heq" for "≍" in [HEq, «term_≍_»]

-@[inherit_doc] infixr:35 " /\\ " => And
-@[inherit_doc] infixr:35 " ∧ "   => And
-@[inherit_doc] infixr:30 " \\/ " => Or
-@[inherit_doc] infixr:30 " ∨  "  => Or
+@[inherit_doc] infixr:35 unicode(" ∧ ", " /\\ ") => And
+@[inherit_doc] infixr:30 unicode(" ∨ ", " \\/ ") => Or
@[inherit_doc] notation:max "¬" p:40 => Not p

 recommended_spelling "and" for "∧" in [And, «term_∧_»]
-/-- prefer `∧` over `/\` -/
-recommended_spelling "and" for "/\\" in [And, «term_/\_»]
 recommended_spelling "or" for "∨" in [Or, «term_∨_»]
-/-- prefer `∨` over `\/` -/
-recommended_spelling "or" for "\\/" in [Or, «term_\/_»]
 recommended_spelling "not" for "¬" in [Not, «term¬_»]

@[inherit_doc] infixl:35 " && " => and
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -63,7 +63,7 @@ meta def expandBracketedBinders (combinatorDeclName : Name) (bracketedExplicitBi
  let combinator := mkCIdentFrom (← getRef) combinatorDeclName
  expandBracketedBindersAux combinator #[bracketedExplicitBinders] body

-syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
+syntax unifConstraint := term unicode(" ≟ ", " =?= ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?

 syntax (docComment)? attrKind "unif_hint" (ppSpace ident)? (ppSpace bracketedBinder)*
@@ -317,7 +317,7 @@ macro_rules
      attribute [instance] $ctor)

 namespace Lean
-syntax cdotTk := patternIgnore("· " <|> ". ")
+syntax cdotTk := unicode("· ", ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic

--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -577,7 +577,7 @@ If `thm` is a theorem `a = b`, then as a rewrite rule,
 * `thm` means to replace `a` with `b`, and
 * `← thm` means to replace `b` with `a`.
 -/
-syntax rwRule    := patternIgnore("← " <|> "<- ")? term
+syntax rwRule    := unicode("← ", "<- ")? term
 /-- A `rwRuleSeq` is a list of `rwRule` in brackets. -/
 syntax rwRuleSeq := " [" withoutPosition(rwRule,*,?) "]"

@@ -653,7 +653,7 @@ A simp lemma specification is:
 * optional `←` to use the lemma backward
 * `thm` for the theorem to rewrite with
 -/
-syntax simpLemma := ppGroup((simpPre <|> simpPost)? patternIgnore("← " <|> "<- ")? term)
+syntax simpLemma := ppGroup((simpPre <|> simpPost)? unicode("← ", "<- ")? term)
 /-- An erasure specification `-thm` says to remove `thm` from the simp set -/
 syntax simpErase := "-" term:max
 /-- The simp lemma specification `*` means to rewrite with all hypotheses -/
@@ -2395,7 +2395,7 @@ If there are several with the same priority, it is uses the "most recent one". E
  cases d <;> rfl
 ```
 -/
-syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? unicode("← ", "<- ")? (ppSpace prio)? : attr

 /--
 Theorems tagged with the `wf_preprocess` attribute are used during the processing of functions defined
@@ -2409,7 +2409,7 @@ that diverges as compiled to be accepted without an explicit `partial` keyword,
 remove irrelevant subterms or change the evaluation order by hiding terms under binders. Therefore
 avoid tagging theorems with `[wf_preprocess]` unless they preserve also operational behavior.
 -/
-syntax (name := wf_preprocess) "wf_preprocess" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := wf_preprocess) "wf_preprocess" (Tactic.simpPre <|> Tactic.simpPost)? unicode("← ", "<- ")? (ppSpace prio)? : attr

 /--
 Theorems tagged with the `method_specs_simp` attribute are used by `@[method_specs]` to further
@@ -2421,7 +2421,7 @@ The `method_specs` theorems are created on demand (using the realizable constant
 this simp set should behave the same in all modules. Do not add theorems to it except in the module
 defining the thing you are rewriting.
 -/
-syntax (name := method_specs_simp) "method_specs_simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := method_specs_simp) "method_specs_simp" (Tactic.simpPre <|> Tactic.simpPost)? unicode("← ", "<- ")? (ppSpace prio)? : attr

 /--
 Register a theorem as a rewrite rule for `cbv` evaluation of a given definition.
@@ -2431,7 +2431,7 @@ You can instruct `cbv` to rewrite the lemma from right-to-left:
@[cbv_eval ←] theorem my_thm : rhs = lhs := ...
 ```
 -/
-syntax (name := cbv_eval) "cbv_eval" patternIgnore("← " <|> "<- ")? (ppSpace ident)? : attr
+syntax (name := cbv_eval) "cbv_eval" unicode("← ", "<- ")? (ppSpace ident)? : attr

 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
--- a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
+++ b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
@@ -24,7 +24,7 @@ macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
  let procDescr := quote s!"simproc set for {procId.getId.toString}"
  -- TODO: better docComment for simprocs
  `($[$doc:docComment]? public meta initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (prio)? : attr
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? unicode("← ", "<- ")? (prio)? : attr
    /-- Simplification procedure -/
    public meta initialize extProc : SimprocExtension ← registerSimprocAttr $(quote procId.getId) $procDescr none
    /-- Simplification procedure -/
--- a/src/Std/Tactic/BVDecide/Syntax.lean
+++ b/src/Std/Tactic/BVDecide/Syntax.lean
@@ -129,7 +129,7 @@ end Tactic
 Theorems tagged with the `bv_normalize` attribute are used during the rewriting step of the
 `bv_decide` tactic.
 -/
-syntax (name := bv_normalize) "bv_normalize" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := bv_normalize) "bv_normalize" (Tactic.simpPre <|> Tactic.simpPost)? unicode("← ", "<- ")? (ppSpace prio)? : attr

 /--
 Auxiliary attribute for builtin `bv_normalize` simprocs.
--- a/tests/elab/ppUnicode.lean
+++ b/tests/elab/ppUnicode.lean
@@ -101,6 +101,30 @@ infixr:35 unicode(" ∨' ", " \\/' ") => Or'
 /-- info: True \/' False : Prop -/
 #guard_msgs in set_option pp.unicode false in #check True \/' False

+/-!
+Testing that core notations respond to `pp.unicode`.
+-/
+/-- info: True ∨ False : Prop -/
+#guard_msgs in set_option pp.unicode true  in #check True ∨ False
+/-- info: True \/ False : Prop -/
+#guard_msgs in set_option pp.unicode false in #check True ∨ False
+/-- info: True ∧ False : Prop -/
+#guard_msgs in set_option pp.unicode true  in #check True ∧ False
+/-- info: True /\ False : Prop -/
+#guard_msgs in set_option pp.unicode false in #check True ∧ False
+/-- info: True → False : Prop -/
+#guard_msgs in set_option pp.unicode true  in #check True → False
+/-- info: True -> False : Prop -/
+#guard_msgs in set_option pp.unicode false in #check True → False
+/-- info: 1 ≤ 2 : Prop -/
+#guard_msgs in set_option pp.unicode true  in #check 1 ≤ 2
+/-- info: 1 <= 2 : Prop -/
+#guard_msgs in set_option pp.unicode false in #check 1 ≤ 2
+/-- info: 1 ≥ 2 : Prop -/
+#guard_msgs in set_option pp.unicode true  in #check 1 ≥ 2
+/-- info: 1 >= 2 : Prop -/
+#guard_msgs in set_option pp.unicode false in #check 1 ≥ 2
+
 /-!
 Tests that used to be in `tests/lean/ppUnicode.lean`.
 -/
--- a/tests/elab/recommendedSpelling.lean
+++ b/tests/elab/recommendedSpelling.lean
@@ -57,7 +57,7 @@ info: some

 /--
 info: some
-  "`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be\nconstructed and destructed like a pair: if `ha : a` and `hb : b` then\n`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `∧` in identifiers is `and`.\n\n * The recommended spelling of `/\\` in identifiers is `and` (prefer `∧` over `/\\`).\n\n * The recommended spelling of `🥤` in identifiers is `bland`."
+  "`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be\nconstructed and destructed like a pair: if `ha : a` and `hb : b` then\n`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `∧` in identifiers is `and`.\n\n * The recommended spelling of `🥤` in identifiers is `bland`."
 -/
 #guard_msgs in
 #eval findDocString? `And