Idris2Doc : Data.OneOf

Data.OneOf

(source)
Reexports
import public Data.List.Elem
import public Data.List.Quantifiers
Definitions
data OneOf : List Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Here : x -> OneOf (x :: xs)
  
There : OneOf xs -> OneOf (x :: xs)
make : Elem a as => a -> OneOf as
  Totality: total
  Visibility: public export
TypeAt : (as : List Type) -> OneOf as -> Type
  Totality: total
  Visibility: public export
Eliminators : List Type -> Type -> Type
  Totality: total
  Visibility: public export
get : (o : OneOf as) -> TypeAt as o
  Totality: total
  Visibility: public export
match : OneOf as -> Eliminators as r -> r
  Totality: total
  Visibility: public export
extend : OneOf as -> OneOf (as ++ bs)
  Totality: total
  Visibility: public export