How to display a backquote in a comment ?

Benoit

unread,

Sep 22, 2022, 11:06:03 AM9/22/22

to Metamath

I am trying to display a backquote in a comment with an <HTML> tag.

The failed attempt appears on https://us.metamath.org/mpeuni/conventions-comments.html where I wanted to display:

...use embedded mathematical symbols when they have been defined (e.g.,` -> ` for [the displayed symbol \rightarrow])

I tried using <pre> ` -> ` </pre> but obviously it didn't work...

(Rk: unrelated, but there is a typo "source source" in that page which has been fixed in a PR)

Thanks for your help,
Benoît

Mario Carneiro

unread,

Sep 22, 2022, 11:17:42 AM9/22/22

to metamath

Did you try doubled backtick? That is, <pre> `` -> `` </pre> if you want to display " ` -> ` " in monospace.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e8b66d1f-f4ed-4606-a6c2-50aa8ef68570n%40googlegroups.com.

Benoit

unread,

Sep 22, 2022, 1:01:55 PM9/22/22

to Metamath

Thanks. Actually, it worked even without the <pre> tag (I think it's ok without monospace).

Benoît

Reply all

Reply to author

Forward