Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Triggers

Documentation

data Triggered a Source #

Constructors

TR Trigger a

Instances

Instances details

Functor Triggered Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods fmap :: (a -> b) -> Triggered a -> Triggered b # (<$) :: a -> Triggered b -> Triggered a #
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 #
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 #
NFData a => NFData (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods rnf :: 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 #
Defunc a => Defunc (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Triggered a -> DF (Triggered a) 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 #
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 #
Store a => Store (Triggered a) Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods size :: Size (Triggered a) # poke :: Triggered a -> Poke () # peek :: Peek (Triggered a) #
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.9.6.3-Fxo1c9HahAZtZcvzlvNkk" '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

Instances details

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 #
Show Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods showsPrec :: Int -> Trigger -> ShowS # show :: Trigger -> String # showList :: [Trigger] -> ShowS #
NFData Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods rnf :: Trigger -> () #
Eq Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods (==) :: Trigger -> Trigger -> Bool # (/=) :: Trigger -> Trigger -> Bool #
PPrint Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods pprintTidy :: Tidy -> Trigger -> Doc Source # pprintPrec :: Int -> Tidy -> Trigger -> Doc Source #
Store Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods size :: Size Trigger # poke :: Trigger -> Poke () # peek :: Peek Trigger #
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.9.6.3-Fxo1c9HahAZtZcvzlvNkk" '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 #