liquid-fixpoint-0.8.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

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

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

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

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

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

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))