numbers in names

Stream: lean4

[Arthur Paulino]

Why can names have numbers? What's the use case for Foo.3.Bar?

[Chris B]

I don't think they can, I'm not able to create a declaration with that name.

[Tomas Skrivan]

Aren't these structure projections?

  def Foo.3.Bar : ℕ := 1 ---  error: expected ':', ':=', 'where' or '|'

[Sebastian Ullrich]

Name.num cannot be generated by surface syntax, it is for internal use only

[Arthur Paulino]

Is such internal use too complicated to understand? Where can I find it?

[Arthur Paulino]

Well, using Tomas' idea I was able make this:

structure QQ where
  Bar : Float

structure Gah where
  nat : Nat
  str : String
  flt : QQ

def Foo : Gah := ⟨1, "hi", ⟨1.2⟩⟩

#eval Foo.3.Bar -- 1.200000

Does that count?

[Sebastian Ullrich]

Probably the simplest use is https://github.com/leanprover/lean4/blob/23fac14b33d1e452020ae5adea85d9ba48a144c8/src/Init/Meta.lean#L201-L212. It's a generator of fresh names. The numeric part guarantees that the name cannot possibly collide with user names.