The thing I found really surprising about Lean is that although it is really focused on proving stuff, it has some surprisingly enormous footguns. What do you think the result of these are?
The first should be a compile time error right, because `UInt8.ofNat` is going to require that its argument is 0-255. And the second should be a compile time error because subtraction should not give a `Nat` unless the first argument is definitely more than the second.
Nope! Both give 0.