verifiable-expressions-0.4.0: An intermediate language for Hoare logic style verification.
Language.Expression.GeneralOp
data GeneralOp op t a where Source #
Constructors
Instances
Methods
hfoldMap :: (forall (b :: k2). t b -> GeneralOp k1 k1 op b) -> h t a -> GeneralOp k1 k1 op a Source #
pretty2 :: Pretty1 (GeneralOp k1 k2 op) t => op t a -> String Source #
prettys2Prec :: Pretty1 (GeneralOp k1 k2 op) t => Int -> op t a -> ShowS Source #
htraverse :: Applicative f => (forall (b :: GeneralOp u u op). t b -> f (t' b)) -> h t a -> f (h t' a) Source #
hsequence :: Applicative f => h (Compose * (GeneralOp u u op) f t) a -> f (h t a) Source #
hmap :: (forall (b :: GeneralOp u u op). t b -> t' b) -> h t a -> h t' a Source #
(+) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal #
(-) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal #
(*) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal #
negate :: WhileExpr l AlgReal -> WhileExpr l AlgReal #
abs :: WhileExpr l AlgReal -> WhileExpr l AlgReal #
signum :: WhileExpr l AlgReal -> WhileExpr l AlgReal #
fromInteger :: Integer -> WhileExpr l AlgReal #
fromString :: String -> WhileExpr s AlgReal #
class EvalOpAt k op where Source #
Minimal complete definition
evalMany
evalMany :: op as r -> Rec k as -> k r Source #
evalMany :: op as r -> Rec Identity WhileOpKind as -> WhileOpKind r Source #
evalMany :: op as r -> Rec SBV WhileOpKind as -> WhileOpKind r Source #
class PrettyOp op where Source #
prettysPrecOp
prettysPrecOp :: Pretty1 t => Int -> op as a -> Rec t as -> ShowS Source #
prettysPrecOp :: Pretty1 WhileOpKind t => Int -> op as a -> Rec WhileOpKind t as -> ShowS Source #