Skip to content

Add ↔︎ with text variation selector as a notation for equivalence. #311

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 5 commits into from
Oct 15, 2026
Merged

Add ↔︎ with text variation selector as a notation for equivalence. #311

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
1d9afc4
Add <-> arrow with text variation selector notation, and test
zacharie-moughanim Sep 21, 2026
16ff129
Merge branch 'rocq-prover:master' into master
zacharie-moughanim Sep 24, 2026
fccda36
Apply suggestion from @proux01
zacharie-moughanim Oct 14, 2026
1cbb2a1
Add comment distinguishing the two equivalence symbols
zacharie-moughanim Oct 14, 2026
865fda3
Update theories/Unicode/Utf8_core.v
zacharie-moughanim Oct 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions theories/Unicode/Utf8.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions theories/Unicode/Utf8_core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,11 @@ 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): 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.

Expand Down
Loading