    {-# LANGUAGE OverloadedStrings, Safe #-}
    module SMTLib2.Int where

    import SMTLib2.AST

    tInt :: Type
    tInt :: Type
    tInt = Ident -> [Type] -> Type
    TApp (Name -> [Integer] -> Ident
    I "Int" []) []

    num :: Integral a => a -> Expr
    num :: a -> Expr
    num a :: a
    a = Literal -> Expr
    Lit (Integer -> Literal
    LitNum (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a))

    nNeg :: Expr -> Expr
    nNeg :: Expr -> Expr
    nNeg x :: Expr
    x = Ident -> [Expr] -> Expr
    app "-" [Expr
    x]

    nSub :: Expr -> Expr -> Expr
    nSub :: Expr -> Expr -> Expr
    nSub x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "-" [Expr
    x,Expr
    y]

    nAdd :: Expr -> Expr -> Expr
    nAdd :: Expr -> Expr -> Expr
    nAdd x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "+" [Expr
    x,Expr
    y]

    nMul :: Expr -> Expr -> Expr
    nMul :: Expr -> Expr -> Expr
    nMul x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "*" [Expr
    x,Expr
    y]

    nDiv :: Expr -> Expr -> Expr
    nDiv :: Expr -> Expr -> Expr
    nDiv x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "div" [Expr
    x,Expr
    y]

    nMod :: Expr -> Expr -> Expr
    nMod :: Expr -> Expr -> Expr
    nMod x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "mod" [Expr
    x,Expr
    y]

    nAbs :: Expr -> Expr
    nAbs :: Expr -> Expr
    nAbs x :: Expr
    x = Ident -> [Expr] -> Expr
    app "abs" [Expr
    x]

    nLeq :: Expr -> Expr -> Expr
    nLeq :: Expr -> Expr -> Expr
    nLeq x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "<=" [Expr
    x,Expr
    y]

    nLt :: Expr -> Expr -> Expr
    nLt :: Expr -> Expr -> Expr
    nLt x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "<" [Expr
    x,Expr
    y]

    nGeq :: Expr -> Expr -> Expr
    nGeq :: Expr -> Expr -> Expr
    nGeq x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app ">=" [Expr
    x,Expr
    y]

    nGt :: Expr -> Expr -> Expr
    nGt :: Expr -> Expr -> Expr
    nGt x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app ">" [Expr
    x,Expr
    y]