Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Documentation
class KnownNat a => KnownIsZero (a :: Nat) where Source #
isZero :: proxy a -> IsZeroCases a Source #
Instances
(KnownNat a, IsZero a ~ 'False, 1 <= a, BVIsNonZero a) => KnownIsZero a Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.IsZero isZero :: proxy a -> IsZeroCases a Source # | |
KnownIsZero 0 Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.IsZero isZero :: proxy 0 -> IsZeroCases 0 Source # |
data IsZeroCases (a :: Nat) where Source #
IsZeroEvidence :: IsZero a ~ 'True => IsZeroCases a | |
NonZeroEvidence :: (IsZero a ~ 'False, BVIsNonZero a, 1 <= a) => IsZeroCases a |
Instances
Show (IsZeroCases a) Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.IsZero showsPrec :: Int -> IsZeroCases a -> ShowS # show :: IsZeroCases a -> String # showList :: [IsZeroCases a] -> ShowS # |