Fcf.Alg.Nat

Fcf.Data.Nat

Documentation

data (==) :: Nat -> Nat -> Exp Bool

Nat equality.

>>> :kind! Eval (2 == 2)
Eval (2 == 2) :: Bool
= 'True

>>> :kind! Eval (2 == 3)
Eval (2 == 3) :: Bool
= 'False

Instances

type Eval (a == b :: Bool -> Type)

Defined in Fcf.Alg.Nat

type Eval (a == b :: Bool -> Type) = Eval ((a <=? b) && (b <=? a))

data (/=) :: Nat -> Nat -> Exp Bool

Nat in-equality.

>>> :kind! Eval (2 /= 2)
Eval (2 /= 2) :: Bool
= 'False

>>> :kind! Eval (2 /= 3)
Eval (2 /= 3) :: Bool
= 'True

Instances

type Eval (a /= b :: Bool -> Type)

Defined in Fcf.Alg.Nat

type Eval (a /= b :: Bool -> Type) = Eval (Eval (a < b) || Eval (b < a))