Mercurial > urweb
comparison lib/ur/monad.urs @ 937:37dd42935dad
Summary row with aggregates
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 15 Sep 2009 10:18:56 -0400 |
parents | 321a2d6feb40 |
children | 8d3aa6c7cee0 |
comparison
equal
deleted
inserted
replaced
936:6966d98c80b5 | 937:37dd42935dad |
---|---|
37 val mapR : K --> m ::: (Type -> Type) -> monad m | 37 val mapR : K --> m ::: (Type -> Type) -> monad m |
38 -> tf :: (K -> Type) | 38 -> tf :: (K -> Type) |
39 -> tr :: (K -> Type) | 39 -> tr :: (K -> Type) |
40 -> (nm :: Name -> t :: K -> tf t -> m (tr t)) | 40 -> (nm :: Name -> t :: K -> tf t -> m (tr t)) |
41 -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) | 41 -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) |
42 | |
43 val mapR2 : K --> m ::: (Type -> Type) -> monad m | |
44 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) | |
45 -> tr :: (K -> Type) | |
46 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) | |
47 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) |