projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
3351499
)
uncomment more of the tutorial
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sun, 27 Mar 2011 19:36:52 +0000
(19:36 +0000)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sun, 27 Mar 2011 19:36:52 +0000
(19:36 +0000)
examples/tutorial.hs
patch
|
blob
|
history
diff --git
a/examples/tutorial.hs
b/examples/tutorial.hs
index
1ac97ae
..
6ef4cbd
100644
(file)
--- 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
class GuestEqChar g where
<[ (==) ]> :: <[ Char -> Char -> Bool ]>@g
-{-
+
staged_accept ::
Regex
-> forall c s.
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) ]>
<[ \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
-- 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) ]>
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 ]>
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 ]>