Cleanup.

DoubleExtensions/Constants.idr

@@ -6,6 +6,7 @@ import DoubleExtensions.Predicates
 ||| 
 public export
 eps : Double
+eps = prim__floatEPSILON
 
 
 ||| 

DoubleExtensions/Postulates.idr

@@ -5,6 +5,10 @@ import Data.So
 import DoubleExtensions.Predicates
 
 
+{- The idea is to postulate properties that are granted by the IEEE
+   standard but that cannot be implemented.
+-}
+
 -- Arithmetic
 
 |||
@@ -17,6 +21,8 @@ public export
 total
 plusZeroRightNeutral : {x : Double} -> x + 0.0 = x
 
+{- What if x = infinity?
+
 ||| 
 public export
 total
@@ -27,17 +33,22 @@ public export
 total
 multZeroRightZero : {x : Double} -> x * 0.0 = 0.0
 
+-}
+
 |||
 public export
 total
 minusSelfZero : {x : Double} -> x - x = 0.0
 
+{- Does not hold
+
 |||
 public export
 total
 plusAssociative : (x : Double) -> (y : Double) -> (z : Double) -> 
                   x + (y + z) = (x + y) + z
 
+-}
 
 -- |LTE|:
 

Set/Set.idr

@@ -36,7 +36,7 @@ implementation Set t (Identity t) where
 
   Elem x (Id y) = x = y
   
-  a1 x = ?kika -- MkSigma (Id x) Refl
+  a1 x = MkSigma (Id x) Refl
 
 
 {-

Sigma/Sigma.idr

 module Sigma.Sigma
 
+{-
 
 public export
 data Sigma : (A : Type) -> (P : A -> Type) -> Type where
   MkSigma : {A : Type} -> {P : A -> Type} -> (x : A) -> (pf : P x) -> Sigma A P
+
+---}
+
+namespace Sigma
+  public export
+  record Sigma a (p : a -> Type) where
+    constructor MkSigma
+    fst : a
+    snd : p fst
+
+