Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Proposal to add a new \<notapprox> symbol ...


view this post on Zulip Email Gateway (May 28 2023 at 21:00):

From: Martin Desharnais <martin.desharnais@posteo.de>
Dear Makarius, dear Isabelle developers,

the Isabelle font contains a glyph for the unicode character "≈" (U+2248
Almost Equal To) usable through the symbol \<approx>.

I propose to add a glyph for its negation "≉" (U+2249 Not Almost Equal
To). For the corresponding symbol name, I propose \<notapprox> similarly
to how we have \<noteq> and \<notin>.

Note that I cannot write ¬(x≈y) instead, as my use case is to define
abbreviations for positive and negative literals in a formalization of
first-order logic with equality.

datatype 'a literal = Pos 'a | Neg 'a

abbreviation pos_eq (infix "≈" 50) where
"t1 ≈ t2 ≡ Pos (Upair t1 t2)"

abbreviation neg_eq (infix "≉" 50) where
"t1 ≉ t2 ≡ Neg (Upair t1 t2)"

Regards,
Martin Desharnais


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (May 29 2023 at 11:21):

From: Lawrence Paulson <lp15@cam.ac.uk>
Looks reasonable to me!

Larry


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 04 2024 at 10:08 UTC