Ascii not (and more)

Stream: new members

[Eric Conlon]

Hi all - How do I find the ASCII version of \not or even not equals? Is there a table with all the common pieces of syntax?

[Ruben Van de Velde]

Why?

[Eric Conlon]

Why \not?

[Kyle Miller]

I don't think Not has an ASCII notation -- you can see the notation defined here: https://github.com/leanprover/lean4/blob/a62d2fd4979671b76b8ab13ccbe4fdf410ec0d9d/src/Init/Notation.lean#L330

It's just notation for the docs#Not function, so the "ASCII" version is the function Not. It will pretty print using the Unicode notation.

[Kyle Miller]

If you want, you can define your own ASCII-only notations, but come join the Unicode party :-)

[Eric Conlon]

Thanks! Notation.lean is helpful. I don't see "not equals" there but I can get by.

[Damiano Testa]

docs#Ne is a tricky one: docs#≠.

[Eric Wieser]

If you have lean open in vscode, you can hover over the notation and it will tell you its ascii name. (edit: not all names are ascii!)

[Adam Topaz]

I’ve seen ~ for not in some old symbolic logic texts. You could add this as custom notation in your project quite easily