bounded UInt8.toUInt64

Stream: new members

[Arthur Paulino]

Hi all, this is probably silly, but I'm not being able to prove this. Help is appreciated!

example (u8 : UInt8) : u8.toUInt64 < 256 := by
  sorry

[Markus Himmel]

example (u8 : UInt8) : u8.toUInt64 < 256 := by
  simpa [UInt64.lt_iff_toNat_lt] using UInt8.toNat_lt _

[Henrik Böving]

Of course also:

import Std.Tactic.BVDecide

example (u8 : UInt8) : u8.toUInt64 < 256 := by
  bv_decide