From dee3eaade170a85f7c2619275e2bdef28038b152 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 30 May 2009 14:44:29 -0400 Subject: Defer pattern-matching exhaustiveness checks and normalize pattern types more thoroughly --- lib/ur/list.ur | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'lib/ur/list.ur') diff --git a/lib/ur/list.ur b/lib/ur/list.ur index 8493f2f5..0776ff30 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -74,6 +74,19 @@ fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = mapM' [] end +fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f = + let + fun mapXM' ls = + case ls of + [] => return + | x :: ls => + this <- f x; + rest <- mapXM' ls; + return {this}{rest} + in + mapXM' + end + fun filter [a] f = let fun fil acc ls = -- cgit v1.2.3