Initial.

Sigma/Operations.lidr

+> module Sigma.Operations
+
+> import Data.Fin
+> import Data.Vect
+
+> import Sigma.Sigma
+> import Finite.Predicates
+> import Decidable.Predicates
+> import Finite.Operations
+> import Vect.Operations
+
+
+> %default total
+
+> %access public export
+
+
+> |||
+> outl : {A : Type} -> {P : A -> Type} -> Sigma A P -> A
+> outl (MkSigma a _) = a
+
+
+> |||
+> outr : {A : Type} -> {P : A -> Type} -> (s : Sigma A P) -> P (outl s)
+> outr (MkSigma _ p) = p
+
+
+> ||| Maps a finite type |A| and a decidable predicate |P| to a vector |Sigma A P| values
+> toVectSigma : {A : Type} ->
+>               {P : A -> Type} ->
+>               Finite A ->
+>               Dec1 P ->
+>               Sigma Nat (\ n => Vect n (Sigma A P))
+> toVectSigma fA d1P = filterTagSigma d1P (toVect fA)
+
+
+> {-
+
+> ---}