Mercurial > meta
diff variant.urs @ 20:296807a9fd50
Variant.foldR and appR
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 02 Jan 2012 17:23:31 -0500 |
parents | 799f43bce62b |
children | e7d64ea0f922 |
line wrap: on
line diff
--- a/variant.urs Sat Dec 31 15:49:54 2011 -0500 +++ b/variant.urs Mon Jan 02 17:23:31 2012 -0500 @@ -24,6 +24,11 @@ val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t +val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t + +val appR : m ::: (Type -> Type) -> monad m + -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {} + val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type -> (p :: K -> f p -> fr p -> t) -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t