Commit 2024-12-20 13:13 ef7c8b7a

refactor(Nat.Prime.Defs): use csimp for Nat.decidablePrime (#19240) previously there were two instances for Decidable (Nat.Prime n), a local one that was kernel-friendly and a non-local one that was compiler friendly. It seems we can have this cake and eat it too by defining the instance to be kernel friendly, and then using csimp to use the other instance when running code natively. It seems to work, given that

set_option trace.compiler.ir.result true in
theorem foo : Prime 31 := by native_decide

prints

[result]
def Nat.foo._nativeDecide_1._closed_1 : u8 :=
  let x_1 : obj := 31;
  let x_2 : u8 := Nat.decidablePrime' x_1;
  ret x_2
def Nat.foo._nativeDecide_1 : u8 :=
  let x_1 : u8 := Nat.foo._nativeDecide_1._closed_1;
  ret x_1