Zulip Chat Archive

Stream: new members

Topic: unexpected token

Michael Beeson (Mar 30 2021 at 02:21):

class  Model (M:Type) :=
(𝟘:M)  --Church zero

"unexpected token" . It doesn't like blackboard-bold zero. Similarly boldface S is "unexpected token". On the other hand
\bbN is refused presumably because it's already defined (but I thought I could still have it for a member of my class, but no).
I don't know the rules for what symbols I may use and I don't know the rules for typing things in different fonts. I'd like to make my
Lean correspond as well as possible to my TeX.

Greg Price (Mar 30 2021 at 02:31):

I think the tool you want is notation. Here's an example from src/category_theory/category/default.lean:

class category_struct (obj : Type u)
extends has_hom.{v} obj : Type (max u (v+1)) :=
(id       : Π X : obj, hom X X)
(comp     : Π {X Y Z : obj}, (X  Y)  (Y  Z)  (X  Z))

notation `𝟙` := category_struct.id -- type as \b1
infixr `  `:80 := category_struct.comp -- type as \gg

Michael Beeson (Mar 30 2021 at 02:51):

OK, it likes

(𝔽:M) -- finite Frege cardinals, least class closed under inhabited successor
(ℕℕ:M) -- Church numbers
(ℍ:M) -- least class closed under nonempty successor

without 'notation', but I need

(ChurchZero:M) --Church zero
(notation: 𝟘:= ChurchZero)

Fine. I can do that. I won't worry about why it needs notation in one case and not in the others.

Curiously the backquotes after 'notation' don't show up here on Zulip. They are there when I click the Edit button...
and I'm not allowed to use just one N for the Church numbers.

Greg Price (Mar 30 2021 at 02:54):

Those backquotes are getting interpreted as part of the markup of the message itself. You can put triple-backticks around the whole code block, and then it'll get formatted as Lean code.

Greg Price (Mar 30 2021 at 02:56):

Next to the edit button, there's a menu which has a "View source" option on anyone's messages (not only your own). So you can use that to see exactly what the markup other people are using looks like.

Michael Beeson (Mar 30 2021 at 03:57):

reserve infix `  ` : 49

class Model (M : Type) :=
(mem : M  M  Prop)
(ℕℕ:M)      -- Church numbers
(ChurchZero:M)  --Church zero
(notation: `𝟘`:= ChurchZero)
(infix   :=  mem)
(S:M  M)  --Church successor
(N_members:  (x:M), (x  ℕℕ   w,(𝟘  w   u, (u  w S u  w)) x  w))

It still doesn't like the zero in the last line, I wonder why?

Greg Price (Mar 30 2021 at 04:35):

Do you have a #mwe? That will make it easier for someone to answer your question.

Greg Price (Mar 30 2021 at 04:35):

(and what's the error you're seeing?)

Eric Wieser (Mar 30 2021 at 07:47):

It's not related to your question, but I'm curious for what T you instantiate instance : model T := sorry for that definition

Kevin Buzzard (Mar 30 2021 at 08:46):

Normally (take a look at for example the definition of a group in mathlib) the way to do this would be to define a notation class has_fancy_zero and then let Model extend this.

Michael Beeson (Mar 30 2021 at 15:45):

That example (I think) IS a MWE, or at least it is a minimal non-working example, and if you change the bb zero in the last line to "ChurchZero", then it works, so that shows the problem is with that one character. What I don't understand is that some non-ascii characters, such as bbF and bbS are accepted without complaint, while others (as in this example) need further work before they can be used. So, which characters/fonts can I use and have them "just work"? As opposed to the related questions about which I care less, "why do some work and some not?" and "how can I make the others work?".

Michael Beeson (Mar 30 2021 at 15:48):

To answer Eric, I never instantiate that class, I just say open Model and develop a theory in which every theorem has parameter M. Of course there are a lot more members of the class than extracted for this example.

Mario Carneiro (Mar 30 2021 at 16:15):

The problem is that bb0 is not an identifier character. If you really want to use it as an identifier and not just a notation you can put it in "french quotes" like \f<<\bb0\f>>

Mario Carneiro (Mar 30 2021 at 16:16):

The set of identifier characters contains some unicode but not all (not most)

Mario Carneiro (Mar 30 2021 at 16:17):

bool is_letter_like_unicode(unsigned u) {
            (0x3b1  <= u && u <= 0x3c9 && u != 0x3bb) || // Lower greek, but lambda
            (0x391  <= u && u <= 0x3A9 && u != 0x3A0 && u != 0x3A3) || // Upper greek, but Pi and Sigma
            (0x3ca  <= u && u <= 0x3fb) ||               // Coptic letters
            (0x1f00 <= u && u <= 0x1ffe) ||              // Polytonic Greek Extended Character Set
            (0x2100 <= u && u <= 0x214f) ||              // Letter like block
            (0x1d49c <= u && u <= 0x1d59f);              // Latin letters, Script, Double-struck, Fractur

double struck letters are identifier characters, but double struck numbers are not

Mario Carneiro (Mar 30 2021 at 16:19):

I'm not sure exactly what the origin of this list of characters is TBH. It is a bit of a hodge-podge; I always just search lean for "coptic" to find it

Mario Carneiro (Mar 30 2021 at 16:20):

However, in mathlib we generally stick to using ascii alphanumerics in identifiers, and only use unicode in notations

Mario Carneiro (Mar 30 2021 at 16:22):

(Aside: should there be a linter for this? Is this desirable? I think there are a few fields named α but I can't think of many other exceptions.)

Mario Carneiro (Mar 30 2021 at 16:24):

ι also shows up in some names in category theory like docs#category_theory.limits.fork.ι_of_ι

Michael Beeson (Apr 11 2021 at 16:33):

I figured out how to determine what symbols Lean can use. Here's how:

  1. Find the symbol you want printed somewhere in Unicode, e.g. in the "symbol tables" in TeXshop.
  2. Paste the desired symbol into Lean.
  3. Hover over it. If Lean can use it, it will pop up instructions how to type it. If those instructions don't pop up,
    then Lean can't cope with that symbol.

Kevin Buzzard (Apr 11 2021 at 18:10):

Does this also apply to notation? For example if you have a symbol you want to use and the instructions don't pop up, can you still define notation for the symbol and then you can use it anyway?

Eric Wieser (Apr 11 2021 at 19:46):

Michael, that isn't a very good heuristic - it relies on the contents of the json file in vscode-lean, which probably contains symbols not used by lean, and frequently needs updating when someone invents new notation

Eric Wieser (Apr 11 2021 at 19:48):

#check (\lam is_this_token_legal_in_a_name, 0) is the reliable way to check if a token is legal in a name.

Last updated: Dec 20 2023 at 11:08 UTC