The native_decide proof of false is broken 😭😭😭

Changes

1 changed files (+2/-0)

• NativeDecide.lean
  • @@ -1,3 +1,5 @@
    + -- Ah darn this no longer works with Lean v4.23 + example : False := by let getHeartbeats (x : Nat) : Nat := let .ok _ state := IO.mkRef x () -- ensure `x` is not eliminated