grisette-0.5.0.1: Symbolic evaluation as a library
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.SymPrim.Prim.Internal.IsZero

Documentation

type family IsZero (a :: Nat) :: Bool where ... Source #

Equations

IsZero 0 = 'True 
IsZero _ = 'False 

class KnownNat a => KnownIsZero (a :: Nat) where Source #

Methods

isZero :: proxy a -> IsZeroCases a Source #

Instances

Instances details
(KnownNat a, IsZero a ~ 'False, 1 <= a, BVIsNonZero a) => KnownIsZero a Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.IsZero

Methods

isZero :: proxy a -> IsZeroCases a Source #

KnownIsZero 0 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.IsZero

Methods

isZero :: proxy 0 -> IsZeroCases 0 Source #

data IsZeroCases (a :: Nat) where Source #

Constructors

IsZeroEvidence :: IsZero a ~ 'True => IsZeroCases a 
NonZeroEvidence :: (IsZero a ~ 'False, BVIsNonZero a, 1 <= a) => IsZeroCases a 

Instances

Instances details
Show (IsZeroCases a) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.IsZero

Methods

showsPrec :: Int -> IsZeroCases a -> ShowS #

show :: IsZeroCases a -> String #

showList :: [IsZeroCases a] -> ShowS #