nothing package:sbv

nothing :: RegExp
sbv Data.SBV.RegExp
Match nothing, universal rejector. 
>>> prove $ \(s :: SString) -> sNot (s `match` nothing)
Q.E.D.
nothingBetweenZeroAndOne :: TP (Proof (Forall "m" Nat -> SBool))
sbv Documentation.SBV.Examples.TP.Peano
>>> runTP nothingBetweenZeroAndOne
Lemma: nothingBetweenZeroAndOne         Q.E.D.
[Proven] nothingBetweenZeroAndOne :: Ɐm ∷ Nat → Bool
isNothing :: SymVal a => SBV (Maybe a) -> SBool
sbv Data.SBV.Maybe
Field recognizer predicate.
sNothing :: SymVal a => SBV (Maybe a)
sbv Data.SBV.Maybe
Symbolic version of the constructor Nothing.