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

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

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

NFData a => NFData (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

rnf :: Triggered a -> ()

Eq a => Eq (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

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

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

Defunc a => Defunc (Triggered a)

Defined in Language.Fixpoint.Defunctionalize

Methods

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

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

PPrint a => PPrint (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Triggered a -> Doc

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

Store a => Store (Triggered a)

Defined in Language.Fixpoint.Types.Triggers

Methods

size :: Size (Triggered a)

poke :: Triggered a -> Poke ()

peek :: Peek (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.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

Constructors

NoTrigger

LeftHandSide

Instances

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

Show Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

showsPrec :: Int -> Trigger -> ShowS

show :: Trigger -> String

showList :: [Trigger] -> ShowS

NFData Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

rnf :: Trigger -> ()

Eq Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

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

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

PPrint Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

pprintTidy :: Tidy -> Trigger -> Doc

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

Store Trigger

Defined in Language.Fixpoint.Types.Triggers

Methods

size :: Size Trigger

poke :: Trigger -> Poke ()

peek :: Peek Trigger

type Rep Trigger

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

noTrigger :: e -> Triggered e

defaultTrigger :: e -> Triggered e

makeTriggers :: Triggered Expr -> [Expr]