More native decide silly stuff

Changes

1 changed files (+11/-2)

• NativeDecide.lean
  • @@ -1,9 +1,18 @@
    - -- Ah darn this no longer works with Lean v4.22 + 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 _ 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