Mercurial > urweb

comparison lib/ur/monad.urs @ 910:8e540df3294d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
grid1 compiles but gets stuck in JS
author Adam Chlipala <adamc@hcoop.net>
date Tue, 25 Aug 2009 13:57:56 -0400
parents 7a4b026e45dd
children 321a2d6feb40
comparison
equal deleted inserted replaced
909:1d3f60e74ec7 910:8e540df3294d
20 -> [[nm] ~ rest] => 20 -> [[nm] ~ rest] =>
21 tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) 21 tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
22 -> tr [] 22 -> tr []
23 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) 23 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
24 24
25 val foldR3 : K --> m ::: (Type -> Type) -> monad m
26 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
27 -> tr :: ({K} -> Type)
28 -> (nm :: Name -> t :: K -> rest :: {K}
29 -> [[nm] ~ rest] =>
30 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
31 -> tr []
32 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
33
25 val mapR : K --> m ::: (Type -> Type) -> monad m 34 val mapR : K --> m ::: (Type -> Type) -> monad m
26 -> tf :: (K -> Type) 35 -> tf :: (K -> Type)
27 -> tr :: (K -> Type) 36 -> tr :: (K -> Type)
28 -> (nm :: Name -> t :: K -> tf t -> m (tr t)) 37 -> (nm :: Name -> t :: K -> tf t -> m (tr t))
29 -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) 38 -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r))