Stream: Beginner Questions

Topic: Typesetting math notation


view this post on Zulip Gergely Buday (Aug 10 2020 at 09:58):

I copied some Coq code into an Isabelle theory file using the verbatim LaTeX environment. The result was this:

Axiom le_antisym : \<forall> x y, x \<le> y \<Rightarrow> y \<le> x \<Rightarrow> x = y.

where le = less or equal sign.

I tried the unicode-math environment suggested here:

https://tex.stackexchange.com/questions/149710/how-to-write-math-symbols-in-a-verbatim

but I guess Isabelle/jEdit already stores the universal quantor as \<forall>.

How can I enter math unicode symbols into the file so that this translation does not occur and I would see these math symbols in their original form?

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:04):

I don't really understand what it is that you want. Can you clarify again?

view this post on Zulip Lukas Stevens (Aug 10 2020 at 10:16):

Save and then reload the file with F5. The symbols should show up in the unicode form. Note that isabelle does not store its theory files with unicode symbols but replaces them with, e.g. \<forall>.

view this post on Zulip Gergely Buday (Aug 10 2020 at 10:45):

@Manuel Eberl I have ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y. in a verbatim environment but the toolchain typesets it as

\<forall> x y, x \<le> y \<Rightarrow> y \<le> x \<Rightarrow> x = y.

The question is: how can I make Isabelle/jEdit to save my unicode symbols as unicode symbols and not as Isabelle ASCII names like \<forall> and \<Rightarrow>?

view this post on Zulip Josh Chen (Aug 10 2020 at 10:50):

(Misunderstood question, deleting unhelpful answer)

view this post on Zulip Josh Chen (Aug 10 2020 at 10:51):

(Misunderstood question, deleting unhelpful answer)

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:55):

I don't understand what you mean by ‘verbatim environment’ and I also don't understand what you mean by ‘toolchain’.

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:56):

If you've ended up with \<Rightarrow> in jEdit somehow and want to get the Unicode display back, try "File → Reload" or, if that doesn't work, "File → Reload with Encoding → UTF-8-Isabelle”.

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:57):

The actual saved file will always contain the expanded ASCII notation (e.g. \<Rightarrow>) and there's not really a way to prevent that, I think. If you do want to get this text, you can of course always just open the file with Isabelle/jEdit and copy out the text as it is displayed there.

view this post on Zulip Gergely Buday (Aug 10 2020 at 10:58):

@Manuel Eberl verbatim environment: \begin{verbatim} LaTeX environment in a text < > block in an Isabelle theory file.

toolchain: the Isabelle document preparation toolchain.

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:58):

(Makarius doesn't like Unicode as a format for actually saving Isabelle source due to several issues such as normalisation and some other reasons I don't remember)

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:58):

Ah, you mean you want to be able to write ∀ in an Isabelle text block and get the corresponding LaTeX character?

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:59):

Try putting the symbols in cartouches

view this post on Zulip Gergely Buday (Aug 10 2020 at 10:59):

Indeed

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:59):

text 
  Foo ‹∀x. P x  Q x Bar

view this post on Zulip Manuel Eberl (Aug 10 2020 at 10:59):

That should work

view this post on Zulip Gergely Buday (Aug 10 2020 at 11:17):

@Manuel Eberl it did the trick (with \tt):

kép.png

Thanks indeed.

view this post on Zulip Manuel Eberl (Aug 10 2020 at 11:23):

It took me a while to realise you were talking about the LaTeX output

view this post on Zulip Gergely Buday (Aug 10 2020 at 11:27):

Sorry for not being clear

view this post on Zulip Manuel Eberl (Aug 10 2020 at 11:34):

No worries!


Last updated: Sep 25 2022 at 23:25 UTC