1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18

import Batteries.Data.UInt

-- Ah darn this no longer works with Lean v4.22
-- Furthermore IO.RealWorld is opaque now so this doesn't compile
-- https://github.com/leanprover/lean4/pull/9631
example : False := by
  let getHeartbeats (x : Nat) : Nat :=
    let .ok _ state := IO.mkRef x () -- ensure `x` is not eliminated
    let .ok val state := IO.getNumHeartbeats state
    val
  have : getHeartbeats 0 ≠ getHeartbeats (0 + 1 - 1) := by native_decide
  simp [getHeartbeats] at this

-- https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Yet.20another.20UInt64.20miscompilation/with/548250126
def danger : UInt64 := UInt64.ofNat UInt64.size - 1
theorem danger_eq_large : danger = 18446744073709551615 := by decide +kernel
theorem danger_eq_one : danger = 1 := by native_decide
theorem bad : False := by simpa using danger_eq_large.symm.trans danger_eq_one