Mercurial > meta
comparison 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 |
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 |