Initial numerals in import paths

Stream: lean4 dev

[Tanner Reese]

It seems that placing numerals at the beginning names in import paths leads to this error

error: build cycle detected:
  +MIL:lean.precompileImports
  +MIL:deps
  +MIL:leanArts
  mil/MIL:leanLib.leanArts
  +MIL:lean.precompileImports

If it is intended that numerals are forbidden at the beginning of names then this is a rather opaque way of indicating that.

[Kim Morrison]

@Mac Malone, is there an existing issue tracking this?