{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Lib.Eq where
import Prelude hiding ((==), (/=))
import qualified Data.Eq as Eq
import Language.Symantic
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.Function (a0)
type instance Sym Eq = Sym_Eq
class Sym_Eq term where
(==) :: Eq a => term a -> term a -> term Bool; infix 4 ==
(/=) :: Eq a => term a -> term a -> term Bool; infix 4 /=
default (==) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool
default (/=) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool
(==) = trans2 (==)
(/=) = trans2 (/=)
instance Sym_Eq Eval where
(==) = eval2 (Eq.==)
(/=) = eval2 (Eq./=)
instance Sym_Eq View where
(==) = viewInfix "==" (infixN 4)
(/=) = viewInfix "/=" (infixN 4)
instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Dup r1 r2) where
(==) = dup2 @Sym_Eq (==)
(/=) = dup2 @Sym_Eq (/=)
instance (Sym_Eq term, Sym_Lambda term) => Sym_Eq (BetaT term)
instance NameTyOf Eq where
nameTyOf _c = ["Eq"] `Mod` "Eq"
instance FixityOf Eq
instance ClassInstancesFor Eq
instance TypeInstancesFor Eq
instance Gram_Term_AtomsFor src ss g Eq
instance (Source src, SymInj ss Eq) => ModuleFor src ss Eq where
moduleFor = ["Eq"] `moduleWhere`
[ "==" `withInfixN` 4 := teEq_eq
, "/=" `withInfixN` 4 := teEq_ne
]
tyEq :: Source src => Type src vs a -> Type src vs (Eq a)
tyEq a = tyConstLen @(K Eq) @Eq (lenVars a) `tyApp` a
teEq_eq, teEq_ne :: TermDef Eq '[Proxy a] (Eq a #> (a -> a -> Bool))
teEq_eq = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (==)
teEq_ne = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (/=)