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}