Operations.idr 247 Bytes
Newer Older
Nicola Botta's avatar
Nicola Botta committed
1
2
3
4
5
6
7
8
9
10
11
12
13
module Sigma.Operations

import Sigma.Sigma


public export
outl : {A : Type} -> {P : A -> Type} -> Sigma A P -> A
outl (MkSigma a _) = a


public export
outr : {A : Type} -> {P : A -> Type} -> (s : Sigma A P) -> P (outl s)
outr (MkSigma _ p) = p