Ssrbool.hs

module Ssrbool where

import qualified Prelude
import qualified Bool
import qualified Datatypes

__ :: any
__ = Prelude.error "Logical or arity value used"

iffP :: Datatypes.Coq_bool -> Bool.Coq_reflect -> Bool.Coq_reflect
iffP _ pb =
  let {_evar_0_ = \_ _ _ -> Bool.ReflectT} in
  let {_evar_0_0 = \_ _ _ -> Bool.ReflectF} in
  case pb of {
   Bool.ReflectT -> _evar_0_ __ __ __;
   Bool.ReflectF -> _evar_0_0 __ __ __}

idP :: Datatypes.Coq_bool -> Bool.Coq_reflect
idP b1 =
  case b1 of {
   Datatypes.Coq_true -> Bool.ReflectT;
   Datatypes.Coq_false -> Bool.ReflectF}

type Coq_pred t = t -> Datatypes.Coq_bool

type Coq_rel t = t -> Coq_pred t