Idris2Doc : Data.DSum

Data.DSum

(source)
A module defining a dependent sum

Reexports

import public Data.DEq
import public Data.DOrd
import public Data.DShow
import public Data.Some

Definitions

data DSum : (a -> Type) -> (a -> Type) -> Type
  A dependent sum
  This data type is supposed to mimic the `DSum` type from Haskells "dependent-sum" package

Totality: total
Visibility: public export
Constructor: 
(:=>) : tag x -> f x -> DSum tag f

Hints:
DEq tag => DEq f => Eq (DSum tag f)
DOrd tag => DOrd f => Ord (DSum tag f)
DShow tag => DShow f => Show (DSum tag f)
fst : DSum tag f -> Some tag
  The first component of a dependent sum

Visibility: export
snd : DSum tag f -> Some f
  The sencond component of a dependent sum

Visibility: export
toSome : DSum tag f -> Some (\x => (tag x, f x))
  Convert a dependent sum to `Some`

Visibility: export