
Meta-data
- Description: Coproducts
- Authors: Dominic Orchard, Vilem-Benjamin Liepelt
- License: BSD3
- Copyright: (c) Authors 2019
- Issue-tracking: https://github.com/dorchard/granule/issues
- Repository: https://github.com/dorchard/granule
Contents
data Either (a : Type) (b : Type) where Left a ; Right b
pushEither : forall {a : Type, b : Type, c : Nat} . {c ≤ 1} => (Either a b) [c] -> Either (a [c]) (b [c])
pullEither : forall {a : Type, b : Type, c : Nat} . Either (a [c]) (b [c]) -> (Either a b) [c]
Distrbute a graded modality outside Either