{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Language.Symantic.Lib.Data.Bool where

-- * Type family 'HBool'
-- | Host-type equality.
type family HEq x y :: Bool where
	HEq x x = 'True
	HEq x y = 'False
-- ** Type 'HBool'
-- | Boolean singleton.
data HBool b where
	HTrue  :: HBool 'True
	HFalse :: HBool 'False
-- ** Class 'Implicit_HBool'
-- | Construct a host-term boolean singleton from a host-type boolean.
class    Implicit_HBool b      where hbool :: HBool b
instance Implicit_HBool 'True  where hbool = HTrue
instance Implicit_HBool 'False where hbool = HFalse