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

    import SMTLib2.AST

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

    num :: Integral a => a -> Expr
    num :: forall a. Integral a => a -> Expr
    num 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 Expr
    x = Ident -> [Expr] -> Expr
    app Ident
    "-" [Expr
    x]

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

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

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

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

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

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

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

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

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

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