Mercurial > urweb
comparison lib/ur/monad.urs @ 2272:b49d22a4eda8
Merge.
author | Ziv Scully <ziv@mit.edu> |
---|---|
date | Sat, 31 Oct 2015 23:35:42 -0400 |
parents | cbd294994c69 |
children |
comparison
equal
deleted
inserted
replaced
2271:85f91c7452b0 | 2272:b49d22a4eda8 |
---|---|
56 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) | 56 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) |
57 -> tr :: (K -> Type) | 57 -> tr :: (K -> Type) |
58 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) | 58 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) |
59 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) | 59 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) |
60 | 60 |
61 val mapR3 : K --> m ::: (Type -> Type) -> monad m | |
62 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) | |
63 -> tr :: (K -> Type) | |
64 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m (tr t)) | |
65 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m ($(map tr r)) | |
66 | |
61 val foldMapR : K --> m ::: (Type -> Type) -> monad m | 67 val foldMapR : K --> m ::: (Type -> Type) -> monad m |
62 -> tf :: (K -> Type) | 68 -> tf :: (K -> Type) |
63 -> tf' :: (K -> Type) | 69 -> tf' :: (K -> Type) |
64 -> tr :: ({K} -> Type) | 70 -> tr :: ({K} -> Type) |
65 -> (nm :: Name -> t :: K -> rest :: {K} | 71 -> (nm :: Name -> t :: K -> rest :: {K} |