From 59454c9766685b381603aaf116bb43a9515dbdba Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 1 Feb 2017 09:24:17 -0500
Subject: Option.app

---
 lib/ur/option.ur  | 5 +++++
 lib/ur/option.urs | 1 +
 2 files changed, 6 insertions(+)

diff --git a/lib/ur/option.ur b/lib/ur/option.ur
index 05c50d1f..baa08466 100644
--- a/lib/ur/option.ur
+++ b/lib/ur/option.ur
@@ -40,6 +40,11 @@ fun mp [a] [b] f x =
         None => None
       | Some y => Some (f y)
 
+fun app [m] [a] (_ : monad m) (f : a -> m {}) x =
+    case x of
+        None => return ()
+      | Some y => f y
+
 fun bind [a] [b] f x =
     case x of
         None => None
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
index 126999a3..c30c40e7 100644
--- a/lib/ur/option.urs
+++ b/lib/ur/option.urs
@@ -9,6 +9,7 @@ val isNone : a ::: Type -> t a -> bool
 val isSome : a ::: Type -> t a -> bool
 
 val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
+val app : m ::: (Type -> Type) -> a ::: Type -> monad m -> (a -> m {}) -> t a -> m {}
 val bind : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
 
 val get : a ::: Type -> a -> option a -> a
-- 
cgit v1.2.3