Add helper function refineMaybe (#267)

agda · Jan 19, 2024 · f37dff8 · f37dff8
1 parent 984821a
commit f37dff8
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/lib/Haskell/Extra/Refinement.agda b/lib/Haskell/Extra/Refinement.agda
@@ -18,3 +18,11 @@ mapRefine : {@0 P Q : a → Set ℓ} (@0 f : ∀ {x} → P x → Q x) → ∃ a
 mapRefine f (x ⟨ p ⟩) = x ⟨ f p ⟩
 
 {-# COMPILE AGDA2HS mapRefine transparent #-}
+
+refineMaybe : {@0 P : a → Set ℓ} 
+            → (mx : Maybe a) → @0 (∀ {x} → mx ≡ Just x → P x)
+            → Maybe (∃ a P)
+refineMaybe Nothing f = Nothing
+refineMaybe (Just x) f = Just (x ⟨ f refl ⟩)
+
+{-# COMPILE AGDA2HS refineMaybe transparent #-}