Good point about overflow - Lean can actually model machine integers with bounded arithmetic operations, allowing you to formally verify these edge cases by explicitly reasoning about overflow behavior.
Do you know of any short examples of this? Yesterday I was trying to prove some "easy" theorems that involved machine number representations, and I couldn't find anything in Lean.
Comments
Good point about overflow - Lean can actually model machine integers with bounded arithmetic operations, allowing you to formally verify these edge cases by explicitly reasoning about overflow behavior.
Do you know of any short examples of this? Yesterday I was trying to prove some "easy" theorems that involved machine number representations, and I couldn't find anything in Lean.