From f0b2422711000c14d5e2e1a8cf49c28a49f03801 Mon Sep 17 00:00:00 2001
From: rnhmjoj <micheleguerinirocco@me.com>
Date: Mon, 28 Nov 2016 21:13:32 +0100
Subject: [PATCH] rebind ifThenElse

---
 Interlude.cabal  |  6 +++---
 src/Data/Bool.hs | 19 ++++++++++++++++++-
 2 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/Interlude.cabal b/Interlude.cabal
index 9881c27..c0e3b24 100644
--- a/Interlude.cabal
+++ b/Interlude.cabal
@@ -13,13 +13,13 @@ cabal-version:       >=1.10
 
 library
   exposed-modules:     Relation.Equality, Data.TypeClass,
-                       Data.Bool, Data.Nat, Data.Integer
+                       Data.Bool, Data.Nat, Data.Fin, Data.Integer
                        Data.Function, Data.Vec
   other-extensions:    GADTs, DataKinds, TypeFamilies, TypeOperators,
                        StandaloneDeriving, ScopedTypeVariables,
                        UndecidableInstances, NoImplicitPrelude,
                        TemplateHaskell, QuasiQuotes, PolyKinds,
-                       UnicodeSyntax
-  build-depends:       base ==4.*, singletons, integer-gmp
+                       UnicodeSyntax, RebindableSyntax
+  build-depends:       base ==4.*, singletons, integer-gmp, ghc-prim
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/src/Data/Bool.hs b/src/Data/Bool.hs
index e28681a..88a3b9d 100644
--- a/src/Data/Bool.hs
+++ b/src/Data/Bool.hs
@@ -9,16 +9,23 @@
 {-# LANGUAGE QuasiQuotes           #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE UnicodeSyntax         #-}
+{-# LANGUAGE RebindableSyntax      #-}
 
 -- | Defines the boolean type and logical operators
 module Data.Bool where
 
+
 import Data.Kind      (Type)
-import Data.TypeClass (Eq, Enum, Show)
+import Data.TypeClass (Eq(..), Enum, Show)
+import GHC.Types      (Bool(..))
 import Data.Singletons.TH
 import Data.Singletons.Prelude.Enum
 
 
+class IfThenElse b where
+  ifThenElse ∷ b -> a -> a -> a
+
+
 singletons [d|
 
   -- | Boolean Type
@@ -49,3 +56,13 @@ singletons [d|
 
   |]
 
+-- | Values equality
+(≡) ∷ Eq a ⇒ a → a → 𝔹
+x ≡ y = case x == y of
+  True  → T
+  False → F
+
+instance IfThenElse 𝔹 where
+  ifThenElse T x y = x
+  ifThenElse F x y = y
+