nothing package:sbv

nothing :: RegExp
sbv Data.SBV.RegExp
Match nothing, universal rejector. 
>>> prove $ \(s :: SString) -> sNot (s `match` nothing)
Q.E.D.
isNothing :: SymVal a => SMaybe a -> SBool
sbv Data.SBV.Maybe
Check if the symbolic value is nothing. 
>>> isNothing (sNothing :: SMaybe Integer)
True

>>> isNothing (sJust (literal "nope"))
False
sNothing :: SymVal a => SMaybe a
sbv Data.SBV.Maybe
The symbolic Nothing. 
>>> sNothing :: SMaybe Integer
Nothing :: SMaybe Integer