From 1d9afc40556189805f5cc7890e252ad22945a05f Mon Sep 17 00:00:00 2001 From: ZachMGH <147696209+zacharie-moughanim@users.noreply.github.com> Date: Mon, 21 Sep 2026 13:44:28 +0200 Subject: [PATCH 1/4] Add <-> arrow with text variation selector notation, and test --- theories/Unicode/Utf8.v | 1 + theories/Unicode/Utf8_core.v | 1 + 2 files changed, 2 insertions(+) diff --git a/theories/Unicode/Utf8.v b/theories/Unicode/Utf8.v index e07cbb5bbc..d8e7b3926d 100644 --- a/theories/Unicode/Utf8.v +++ b/theories/Unicode/Utf8.v @@ -19,6 +19,7 @@ Notation "x ≥ y" := (ge x y) (at level 70, no associativity). (* Check ∀ x z, True -> (∃ y v, x + v ≥ y + z) ∨ x ≤ 0. *) +(* Check ∀ P, P ↔︎ P. *) (* Integer Arithmetic *) (* TODO: this should come after ZArith diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v index ec63022004..3754a212fb 100644 --- a/theories/Unicode/Utf8_core.v +++ b/theories/Unicode/Utf8_core.v @@ -25,6 +25,7 @@ Notation "x → y" := (x -> y) (at level 99, y at level 200, right associativity): type_scope. Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope. +Notation "x ↔︎ y" := (x <-> y) (at level 95, no associativity): type_scope. Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope. Notation "x ≠ y" := (x <> y) (at level 70) : type_scope. From fccda363019542b84f95f471bb7e421c8e32858f Mon Sep 17 00:00:00 2001 From: ZacharieMGH <147696209+zacharie-moughanim@users.noreply.github.com> Date: Wed, 14 Oct 2026 17:09:21 +0200 Subject: [PATCH 2/4] Apply suggestion from @proux01 Co-authored-by: Pierre Roux --- theories/Unicode/Utf8_core.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v index 3754a212fb..8cdd9dfc8c 100644 --- a/theories/Unicode/Utf8_core.v +++ b/theories/Unicode/Utf8_core.v @@ -24,7 +24,7 @@ Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope. Notation "x → y" := (x -> y) (at level 99, y at level 200, right associativity): type_scope. -Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope. +Notation "x ↔ y" := (x <-> y) (at level 95, no associativity, only parsing): type_scope. Notation "x ↔︎ y" := (x <-> y) (at level 95, no associativity): type_scope. Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope. Notation "x ≠ y" := (x <> y) (at level 70) : type_scope. From 1cbb2a16e9ae4fb95eef7df0843327e46f125f78 Mon Sep 17 00:00:00 2001 From: ZachMGH <147696209+zacharie-moughanim@users.noreply.github.com> Date: Wed, 14 Oct 2026 18:48:49 +0200 Subject: [PATCH 3/4] Add comment distinguishing the two equivalence symbols --- theories/Unicode/Utf8_core.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v index 8cdd9dfc8c..f1425b746d 100644 --- a/theories/Unicode/Utf8_core.v +++ b/theories/Unicode/Utf8_core.v @@ -24,6 +24,9 @@ Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope. Notation "x → y" := (x -> y) (at level 99, y at level 200, right associativity): type_scope. +(* The two following differ in that the second symbol "↔︎" is the + symbol "↔" from the first line, appended with + the _text variation selector_, indicating that it must be displayed as text and not emoji. *) Notation "x ↔ y" := (x <-> y) (at level 95, no associativity, only parsing): type_scope. Notation "x ↔︎ y" := (x <-> y) (at level 95, no associativity): type_scope. Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope. From 865fda3baf3a6398c33f9f10791c780276f66551 Mon Sep 17 00:00:00 2001 From: ZacharieMGH <147696209+zacharie-moughanim@users.noreply.github.com> Date: Thu, 15 Oct 2026 11:06:02 +0200 Subject: [PATCH 4/4] Update theories/Unicode/Utf8_core.v Co-authored-by: Pierre Roux --- theories/Unicode/Utf8_core.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v index f1425b746d..dc84783fd7 100644 --- a/theories/Unicode/Utf8_core.v +++ b/theories/Unicode/Utf8_core.v @@ -27,8 +27,8 @@ Notation "x → y" := (x -> y) (* The two following differ in that the second symbol "↔︎" is the symbol "↔" from the first line, appended with the _text variation selector_, indicating that it must be displayed as text and not emoji. *) -Notation "x ↔ y" := (x <-> y) (at level 95, no associativity, only parsing): type_scope. -Notation "x ↔︎ y" := (x <-> y) (at level 95, no associativity): type_scope. +Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope. +Notation "x ↔︎ y" := (x <-> y) (at level 95, no associativity, only parsing): type_scope. Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope. Notation "x ≠ y" := (x <> y) (at level 70) : type_scope.