{-# LANGUAGE OverloadedStrings, Safe #-} module SMTLib2.Array where import SMTLib2.AST tArray :: Type -> Type -> Type tArray :: Type -> Type -> Type tArray x :: Type x y :: Type y = Ident -> [Type] -> Type TApp "Array" [Type x,Type y] select :: Expr -> Expr -> Expr select :: Expr -> Expr -> Expr select x :: Expr x y :: Expr y = Ident -> [Expr] -> Expr app "select" [Expr x,Expr y] store :: Expr -> Expr -> Expr -> Expr store :: Expr -> Expr -> Expr -> Expr store x :: Expr x y :: Expr y z :: Expr z = Ident -> [Expr] -> Expr app "store" [Expr x,Expr y,Expr z]