From 522b368f6a38d1b9589645621a672921ad071a4f Mon Sep 17 00:00:00 2001 From: marcusrossel Date: Fri, 4 Sep 2026 13:17:13 +0200 Subject: [PATCH] feat: add a `Decidable` instance for `bif` (`cond`) --- src/Init/Core.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 4dd675cb9c04..23e784c3806b 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1230,6 +1230,12 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : | isTrue hc => dT hc | isFalse hc => dE hc +@[macro_inline] +instance {c : Bool} {t e : Prop} [dT : Decidable t] [dE : Decidable e] : Decidable (bif c then t else e) := + match c with + | true => dT + | false => dE + /-- Auxiliary definition for generating compact `noConfusion` for enumeration types -/ abbrev noConfusionTypeEnum {α : Sort u} (f : α → Nat) (P : Sort w) (x y : α) : Sort w := ((f x).beq (f y)).casesOn P (P → P)