{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
module Fcf.Alg.Nat where
import qualified GHC.TypeNats as TN
import Fcf.Core (Eval, Exp)
import Fcf.Data.Bool
import Fcf.Data.Nat (Nat)
import qualified Fcf.Data.Nat as FN
data (==) :: Nat -> Nat -> Exp Bool
type instance Eval ((==) a b) = Eval ((a TN.<=? b) && (b TN.<=? a))
data (/=) :: Nat -> Nat -> Exp Bool
type instance Eval ((/=) a b) = Eval (Eval (a FN.< b) || Eval (b FN.< a))