{-# LANGUAGE Trustworthy #-}
module SBool.DeFun (
LAnd, LAndSym, LAndSym1,
land, landSym, landSym1,
LOr, LOrSym, LOrSym1,
lor, lorSym, lorSym1,
Not, NotSym,
not, notSym,
) where
import Data.Singletons.Bool (SBool (..), sboolAnd, sboolNot, sboolOr)
import DeFun.Bool
import DeFun.Core
land :: SBool x -> SBool y -> SBool (LAnd x y)
land :: forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LAnd x y)
land = forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LAnd x y)
sboolAnd
landSym1 :: SBool x -> Lam SBool SBool (LAndSym1 x)
landSym1 :: forall (x :: Bool). SBool x -> Lam SBool SBool (LAndSym1 x)
landSym1 SBool x
x = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LAnd x y)
land SBool x
x)
landSym :: Lam2 SBool SBool SBool LAndSym
landSym :: Lam2 SBool SBool SBool LAndSym
landSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall (x :: Bool). SBool x -> Lam SBool SBool (LAndSym1 x)
landSym1
lor :: SBool x -> SBool y -> SBool (LOr x y)
lor :: forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LOr x y)
lor = forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LOr x y)
sboolOr
lorSym1 :: SBool x -> Lam SBool SBool (LOrSym1 x)
lorSym1 :: forall (x :: Bool). SBool x -> Lam SBool SBool (LOrSym1 x)
lorSym1 SBool x
x = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LOr x y)
lor SBool x
x)
lorSym :: Lam2 SBool SBool SBool LOrSym
lorSym :: Lam2 SBool SBool SBool LOrSym
lorSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall (x :: Bool). SBool x -> Lam SBool SBool (LOrSym1 x)
lorSym1
not :: SBool x -> SBool (Not x)
not :: forall (x :: Bool). SBool x -> SBool (Not x)
not = forall (x :: Bool). SBool x -> SBool (Not x)
sboolNot
notSym :: Lam SBool SBool NotSym
notSym :: Lam SBool SBool NotSym
notSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall (x :: Bool). SBool x -> SBool (Not x)
not