From 71ff36621103dfab119dfbead39dea3995d5832d Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 9 Mar 2026 15:17:32 -0700 Subject: [PATCH] feat: use `unicode(...)` in Init/Notation and elsewhere (#10384) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/Init/Conv.lean | 2 +- src/Init/Grind/Interactive.lean | 2 +- src/Init/Notation.lean | 39 +++++++------------ src/Init/NotationExtra.lean | 4 +- src/Init/Tactics.lean | 12 +++--- .../Meta/Tactic/Simp/RegisterCommand.lean | 2 +- src/Std/Tactic/BVDecide/Syntax.lean | 2 +- tests/elab/ppUnicode.lean | 24 ++++++++++++ tests/elab/recommendedSpelling.lean | 2 +- 9 files changed, 52 insertions(+), 37 deletions(-) diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 13d983226b..cb1f7177ca 100644 --- 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. -/ diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean index 4803b54848..007cf7ce83 100644 --- 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, diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 8870ff316c..86e95cd066 100644 --- 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 diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 2742ef0f8a..bf509c6872 100644 --- 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 diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 1dc46d0b25..6d64e968cc 100644 --- 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" diff --git a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean index dda1c7a232..6e37d3983a 100644 --- 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 -/ diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean index 329bb5cc9f..8ee44b66cb 100644 --- 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. diff --git a/tests/elab/ppUnicode.lean b/tests/elab/ppUnicode.lean index b8df011fbd..0fa450fe5d 100644 --- 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`. -/ diff --git a/tests/elab/recommendedSpelling.lean b/tests/elab/recommendedSpelling.lean index ea1803fd85..8be5040e80 100644 --- 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