aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/monad.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-07-19 17:45:02 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-07-19 17:45:02 -0400
commit94a1373401529f500640b0c0628e7173612cdabe (patch)
tree89ce0f6149e50fdfece4b083c2be2033c7727c63 /lib/ur/monad.urs
parent19cd9e965929d541e6714f62154f01b9e487a712 (diff)
Working on Grid; have gone from one dynamic table bizareness to another
Diffstat (limited to 'lib/ur/monad.urs')
-rw-r--r--lib/ur/monad.urs3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs
index cfe0ef8e..b3cb3d6f 100644
--- a/lib/ur/monad.urs
+++ b/lib/ur/monad.urs
@@ -1,2 +1,5 @@
val exec : m ::: (Type -> Type) -> monad m -> ts ::: {Type}
-> $(map m ts) -> folder ts -> m $ts
+
+val ignore : m ::: (Type -> Type) -> monad m -> t ::: Type
+ -> m t -> m unit