X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=examples%2Ftutorial.hs;h=6ef4cbd29a66e426b10ecbf11acb5fce71ad82b6;hb=d51e5dc2fcc6b6c7d40aa45397925dc3444c3dbb;hp=1ac97ae3265eb7bb200b161be2bf33a4f3c2fab4;hpb=70939a4eb9560ceeea3e9cf176ac5a36f9201ac4;p=coq-hetmet.git diff --git a/examples/tutorial.hs b/examples/tutorial.hs index 1ac97ae..6ef4cbd 100644 --- a/examples/tutorial.hs +++ b/examples/tutorial.hs @@ -384,7 +384,7 @@ class GuestStream g a where class GuestEqChar g where <[ (==) ]> :: <[ Char -> Char -> Bool ]>@g -{- + staged_accept :: Regex -> forall c s. @@ -419,7 +419,7 @@ staged_accept (Const c) k = <[ \s -> if gs_empty s then false else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]> --} + -- this type won't work unless the case for (Star e) is commented out; -- see loop above @@ -451,7 +451,7 @@ instance Category Code where id = Code <[ \x -> x ]> f . g = Code <[ \x -> ~~(unCode f) (~~(unCode g) x) ]> -instance GArrow Code (,) where +instance GArrow Code (,) () where ga_first f = Code <[ \(x,y) -> ((~~(unCode f) x),y) ]> ga_second f = Code <[ \(x,y) -> (x ,(~~(unCode f) y)) ]> ga_cancell = Code <[ \(_,x) -> x ]>