Currently, we recognize well-known tokens like u32 and lower them to Lean as U32, which means we aren't robust against e.g. type u32 = u8;. We should fix this or at least warn very loudly about it.
Presumably analyzing LLBC directly (#3040) would partially resolve this concern.
Currently, we recognize well-known tokens like
u32and lower them to Lean asU32, which means we aren't robust against e.g.type u32 = u8;. We should fix this or at least warn very loudly about it.Presumably analyzing LLBC directly (#3040) would partially resolve this concern.