Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Triggers

Documentation

data Triggered a Source #

Constructors

TR Trigger a

Instances

Functor Triggered Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods fmap :: (a -> b) -> Triggered a -> Triggered b # (<$) :: a -> Triggered b -> Triggered a #
Eq a => Eq (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods (==) :: Triggered a -> Triggered a -> Bool # (/=) :: Triggered a -> Triggered a -> Bool #
Show a => Show (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods showsPrec :: Int -> Triggered a -> ShowS # show :: Triggered a -> String # showList :: [Triggered a] -> ShowS #
Generic (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Associated Types type Rep (Triggered a) :: Type -> Type # Methods from :: Triggered a -> Rep (Triggered a) x # to :: Rep (Triggered a) x -> Triggered a #
Binary a => Binary (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods put :: Triggered a -> Put # get :: Get (Triggered a) # putList :: [Triggered a] -> Put #
NFData a => NFData (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods rnf :: Triggered a -> () #
PPrint a => PPrint (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods pprintTidy :: Tidy -> Triggered a -> Doc Source # pprintPrec :: Int -> Tidy -> Triggered a -> Doc Source #
SMTLIB2 (Triggered Expr) Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Triggered Expr -> Builder Source #
Elaborate e => Elaborate (Triggered e) Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: Located String -> SymEnv -> Triggered e -> Triggered e Source #
Defunc a => Defunc (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Triggered a -> DF (Triggered a) Source #
type Rep (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers type Rep (Triggered a) = D1 (MetaData "Triggered" "Language.Fixpoint.Types.Triggers" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "TR" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Trigger) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))

data Trigger Source #

Constructors

NoTrigger
LeftHandSide

Instances

Eq Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods (==) :: Trigger -> Trigger -> Bool # (/=) :: Trigger -> Trigger -> Bool #
Show Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods showsPrec :: Int -> Trigger -> ShowS # show :: Trigger -> String # showList :: [Trigger] -> ShowS #
Generic Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Associated Types type Rep Trigger :: Type -> Type # Methods from :: Trigger -> Rep Trigger x # to :: Rep Trigger x -> Trigger #
Binary Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods put :: Trigger -> Put # get :: Get Trigger # putList :: [Trigger] -> Put #
NFData Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods rnf :: Trigger -> () #
PPrint Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods pprintTidy :: Tidy -> Trigger -> Doc Source # pprintPrec :: Int -> Tidy -> Trigger -> Doc Source #
type Rep Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers type Rep Trigger = D1 (MetaData "Trigger" "Language.Fixpoint.Types.Triggers" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "NoTrigger" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "LeftHandSide" PrefixI False) (U1 :: Type -> Type))

noTrigger :: e -> Triggered e Source #

defaultTrigger :: e -> Triggered e Source #

makeTriggers :: Triggered Expr -> [Expr] Source #