Sigma.lidr 172 Bytes
Newer Older
Nicola Botta's avatar
Cleanup  
Nicola Botta committed
1
2
3
4
5
6
7
8
9
10
11
> module Sigma.Sigma


> namespace Sigma
>   public export
>   record Sigma (A : Type) (P : A -> Type) where
>     constructor MkSigma
>     outl : A
>     outr : P outl