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