Mercurial > meta

comparison variant.urs @ 20:296807a9fd50

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Variant.foldR and appR
author Adam Chlipala <adam@chlipala.net>
date Mon, 02 Jan 2012 17:23:31 -0500
parents 799f43bce62b
children e7d64ea0f922
comparison
equal deleted inserted replaced
19:875221eee987 20:296807a9fd50
22 -> f t 22 -> f t
23 -> variant (map f r) 23 -> variant (map f r)
24 24
25 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t 25 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
26 26
27 val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t
28
29 val appR : m ::: (Type -> Type) -> monad m
30 -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {}
31
27 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type 32 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
28 -> (p :: K -> f p -> fr p -> t) 33 -> (p :: K -> f p -> fr p -> t)
29 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t 34 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t
30 35
31 val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type 36 val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type