Language.Fixpoint.Types.Triggers

Documentation

data Triggered a

Constructors

TR Trigger a

Instances

Functor Triggered

Defined in Language.Fixpoint.Types.Triggers

Methods

fmap :: (a -> b) -> Triggered a -> Triggered b

(<$) :: a -> Triggered b -> Triggered a

Eq a => Eq (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

(==) :: Triggered a -> Triggered a -> Bool

(/=) :: Triggered a -> Triggered a -> Bool

Show a => Show (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

showsPrec :: Int -> Triggered a -> ShowS

show :: Triggered a -> String

showList :: [Triggered a] -> ShowS

Generic (Triggered a)

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)

Defined in Language.Fixpoint.Types.Triggers

Methods

put :: Triggered a -> Put

get :: Get (Triggered a)

putList :: [Triggered a] -> Put

NFData a => NFData (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

rnf :: Triggered a -> ()

PPrint a => PPrint (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Triggered a -> Doc

pprintPrec :: Int -> Tidy -> Triggered a -> Doc

SMTLIB2 (Triggered Expr)

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Triggered Expr -> Builder

Elaborate e => Elaborate (Triggered e)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Triggered e -> Triggered e

Defunc a => Defunc (Triggered a)

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Triggered a -> DF (Triggered a)

type Rep (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

type Rep (Triggered a) = D1 ('MetaData "Triggered" "Language.Fixpoint.Types.Triggers" "liquid-fixpoint-0.8.10.2-inplace" '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

Constructors

NoTrigger

LeftHandSide

Instances

Eq Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

(==) :: Trigger -> Trigger -> Bool

(/=) :: Trigger -> Trigger -> Bool

Show Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

showsPrec :: Int -> Trigger -> ShowS

show :: Trigger -> String

showList :: [Trigger] -> ShowS

Generic Trigger

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

Defined in Language.Fixpoint.Types.Triggers

Methods

put :: Trigger -> Put

get :: Get Trigger

putList :: [Trigger] -> Put

NFData Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

rnf :: Trigger -> ()

PPrint Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Trigger -> Doc

pprintPrec :: Int -> Tidy -> Trigger -> Doc

type Rep Trigger

Defined in Language.Fixpoint.Types.Triggers

type Rep Trigger = D1 ('MetaData "Trigger" "Language.Fixpoint.Types.Triggers" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "NoTrigger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LeftHandSide" 'PrefixI 'False) (U1 :: Type -> Type))

noTrigger :: e -> Triggered e

defaultTrigger :: e -> Triggered e

makeTriggers :: Triggered Expr -> [Expr]