Induction with type U32

Stream: new members

[adem bizid]

Hi everyone,
Recently, I was trying to prove some code in Rust using lean4 and I was struggling to use induction with type u32. Using Nat works fine for me. However, using u32 the code throws errors. Also, is there a way to convert U32 to UInt32 or to Nat?
Thanks in advance for your help.

[Kim Morrison]

You might have to explain in more detail what you are doing. docs#U32 is not a built-in type.

[adem bizid]

I converted Rust code to Lean4 using Aeneas tool. The resulting code uses the U32 type. Are you saying that the only way to prove the code is to first change the type from U32 to UInt32 or Nat as U32 is not built in?

[Eric Wieser]

I think what Kim is saying is that you weren't telling us what U32 was. Could you point to the lines in Aeneas that define it?

[Notification Bot]

This topic was moved here from #maths > Induction with type U32 by Patrick Massot.

[eyelash]

I'm not familiar with Aeneas but I found a function U32.toNat here that seems to convert U32 to Nat.