Identifier with number

Stream: lean4

[Marcus Rossel]

Is it possible to use identifiers with numbers in them for the def or inductive commands - e.g. inductive Foo.1.Bar?
I tried:

open Lean in
macro "gen" : command => do
  let i := mkIdent $ .str (.num (.str .anonymous "x") 1) "y"
  `(inductive $i)

gen -- invalid 'end', insufficient scopes

[James Gallicchio]

I think numbers right after the dot are reserved for projections? But you can do ._1

[James Gallicchio]

There was a description somewhere in the metaprogramming tutorial about how .num is reserved for internal use, I don't remember for what exactly