Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
This formulation of LTL is in positive normal form by construction, and trivially dualizable. This choice was driven by the following Coq formalization, showing that all the laws for LTL hold under a denotation from this structure into Coq's logic, over all finite lists:
https://github.com/jwiegley/constructive-ltl/blob/master/src/LTL.v#L69
Documentation
HitBottom String | |
Rejected a | |
BothFailed (Reason a) (Reason a) | |
LeftFailed (Reason a) | |
RightFailed (Reason a) |
Instances
Instances
Show a => Show (Result a) Source # | |
Generic (Result a) Source # | |
NFData a => NFData (Result a) Source # | |
type Rep (Result a) Source # | |
Defined in LTL type Rep (Result a) = D1 (MetaData "Result" "LTL" "simple-ltl-1.0.0-Fb9CmHs9o9MCVdA6TpcRen" False) (C1 (MetaCons "Failure" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Reason a))) :+: C1 (MetaCons "Success" PrefixI False) (U1 :: Type -> Type)) |
eventually :: LTL a -> LTL a Source #