From bd0d3db78996b00e153252f03b02551ac3fde4cf 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