From ee9fcd30e87f11a22541a48a1e850ac4629f5171 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Feb 2022 12:00:29 -0800 Subject: [PATCH] fix: mark `Nat.decEq` as `[reducible]` It is used by the `noConfusionType` construction for enumeration types, and we want it to reduce even when the reducibility setting is `TransparencyMode.reducible` as for other inductive types. see issue #1016 --- src/Init/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 24595e9b8e..5967ad8dc1 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -616,7 +616,7 @@ theorem Nat.ne_of_beq_eq_false : {n m : Nat} → Eq (beq n m) false → Not (Eq have : Eq (beq n m) false := h₁ Nat.noConfusion h₂ (fun h₂ => absurd h₂ (ne_of_beq_eq_false this)) -@[extern "lean_nat_dec_eq"] +@[reducible, extern "lean_nat_dec_eq"] protected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) := match h:beq n m with | true => isTrue (eq_of_beq_eq_true h)