Skip to content

Commit

Permalink
Add fromMaybe to Haskell.Data.Maybe
Browse files Browse the repository at this point in the history
  • Loading branch information
HeinrichApfelmus committed May 9, 2024
1 parent aae2c3f commit 9fbcd5b
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 0 deletions.
5 changes: 5 additions & 0 deletions lib/customer-deposit-wallet-pure/agda/Haskell/Data/Maybe.agda
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,11 @@ catMaybes [] = []
catMaybes (Nothing ∷ xs) = catMaybes xs
catMaybes (Just x ∷ xs) = x ∷ catMaybes xs

fromMaybe : {a : Set} a Maybe a a
fromMaybe _ (Just a) = a
fromMaybe a Nothing = a

{-# COMPILE AGDA2HS isNothing #-}
{-# COMPILE AGDA2HS isJust #-}
{-# COMPILE AGDA2HS catMaybes #-}
{-# COMPILE AGDA2HS fromMaybe #-}
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,7 @@ catMaybes [] = []
catMaybes (Nothing : xs) = catMaybes xs
catMaybes (Just x : xs) = x : catMaybes xs

fromMaybe :: a -> Maybe a -> a
fromMaybe _ (Just a) = a
fromMaybe a Nothing = a

0 comments on commit 9fbcd5b

Please sign in to comment.