liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

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

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

Elaborate e => Elaborate (Triggered e) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

PPrint a => PPrint (Triggered a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Triggers

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.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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

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

Store Trigger Source # 
Instance details

Defined in Language.Fixpoint.Types.Triggers

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.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "NoTrigger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LeftHandSide" 'PrefixI 'False) (U1 :: Type -> Type))