unexpected token

Stream: new members

[Michael Beeson]

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]

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]

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]

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]

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]

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]

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

[Greg Price]

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

[Eric Wieser]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

bool is_letter_like_unicode(unsigned u) {
    return
            (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]

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]

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

[Mario Carneiro]

(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]

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

[Michael Beeson]

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]

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]

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]

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