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