Unexpected name clash

[sonmarcho]

trafficstars

Reported by Anders Larsson in the zulip:

pub fn byteToWord (n: u8) -> u16 {
    n.into()
}

triggers:

[Info ] Generated the partial file (because of errors): ./Mylib.lean
[Error] Name clash detected: the following identifiers are bound to the same name "core.convert.Into":
- trait_decl_id: 0
  Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/convert/mod.rs', lines 444:0-444:24
- trait_impl_id: 0
  Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/convert/mod.rs', lines 444:0-444:24
You may want to rename some of your definitions, or report an issue.
[Error] Error when registering the name for id: trait_impl_id: 0:
The chosen name is already in the names set: core.convert.Into
Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/convert/mod.rs', lines 444:0-444:24