From 48aacea0b9adc548c47fd46b9addd6b84e3a5272 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Wed, 24 Jan 2024 10:43:38 +0100
Subject: [PATCH] Add `ifDec` function for branching on a `Dec` that compiles
 to `if`

---
 lib/Haskell/Extra/Dec.agda | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/lib/Haskell/Extra/Dec.agda b/lib/Haskell/Extra/Dec.agda
index f50c2621..5b2bd810 100644
--- a/lib/Haskell/Extra/Dec.agda
+++ b/lib/Haskell/Extra/Dec.agda
@@ -41,3 +41,7 @@ mapDec : @0 (a → b)
 mapDec f g (True  ⟨ x ⟩) = True  ⟨ f x   ⟩
 mapDec f g (False ⟨ h ⟩) = False ⟨ h ∘ g ⟩
 {-# COMPILE AGDA2HS mapDec transparent #-}
+
+ifDec : Dec a → (@0 {{a}} → b) → (@0 {{a → ⊥}} → b) → b
+ifDec (b ⟨ p ⟩) x y = if b then (λ where {{refl}} → x {{p}}) else (λ where {{refl}} → y {{p}})
+{-# COMPILE AGDA2HS ifDec inline #-}