verifiable-expressions-0.6.0: An intermediate language for Hoare logic style verification.

Safe HaskellNone
LanguageHaskell2010

Language.Expression.GeneralOp

Documentation

data GeneralOp op t a where Source #

Constructors

Op :: op as r -> Rec t as -> GeneralOp op t r 
Instances
EvalOpAt k2 op => HFoldableAt (k2 :: k1 -> Type) (GeneralOp op :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

hfoldMap :: (forall (b :: k). t b -> k2 b) -> GeneralOp op t a -> k2 a Source #

PrettyOp op => Pretty2 (GeneralOp op :: (k1 -> Type) -> k2 -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

pretty2 :: Pretty1 t => GeneralOp op t a -> String Source #

prettys2Prec :: Pretty1 t => Int -> GeneralOp op t a -> ShowS Source #

HTraversable (GeneralOp op :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

htraverse :: Applicative f => (forall (b :: u0). t b -> f (t' b)) -> GeneralOp op t a -> f (GeneralOp op t' a) Source #

hsequence :: Applicative f => GeneralOp op (Compose f t) a -> f (GeneralOp op t a) Source #

HFunctor (GeneralOp op :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

hmap :: (forall (b :: u0). t b -> t' b) -> GeneralOp op t a -> GeneralOp op t' a Source #

Num (WhileExpr l AlgReal) Source # 
Instance details

Defined in Language.While.Syntax

IsString s => IsString (WhileExpr s AlgReal) Source # 
Instance details

Defined in Language.While.Syntax

class EvalOpAt k op where Source #

Methods

evalMany :: op as r -> Rec k as -> k r Source #

Instances
EvalOpAt Identity WhileOpKind Source # 
Instance details

Defined in Language.While.Syntax

Methods

evalMany :: WhileOpKind as r -> Rec Identity as -> Identity r Source #

EvalOpAt SBV WhileOpKind Source # 
Instance details

Defined in Language.While.Syntax

Methods

evalMany :: WhileOpKind as r -> Rec SBV as -> SBV r Source #

class PrettyOp op where Source #

Methods

prettysPrecOp :: Pretty1 t => Int -> op as a -> Rec t as -> ShowS Source #

Instances
PrettyOp WhileOpKind Source # 
Instance details

Defined in Language.While.Syntax

Methods

prettysPrecOp :: Pretty1 t => Int -> WhileOpKind as a -> Rec t as -> ShowS Source #