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

    import SMTLib2.AST

    tBool :: Type
    tBool :: Type
    tBool = Type
    "Bool"

    true :: Expr
    true :: Expr
    true = Ident -> [Expr] -> Expr
    app Ident
    "true" []

    false :: Expr
    false :: Expr
    false = Ident -> [Expr] -> Expr
    app Ident
    "false" []

    not :: Expr -> Expr
    not :: Expr -> Expr
    not Expr
    p = Ident -> [Expr] -> Expr
    app Ident
    "not" [Expr
    p]

    (==>) :: Expr -> Expr -> Expr
    Expr
    p ==> :: Expr -> Expr -> Expr
    ==> Expr
    q = Ident -> [Expr] -> Expr
    app Ident
    "=>" [Expr
    p,Expr
    q]

    and :: Expr -> Expr -> Expr
    and :: Expr -> Expr -> Expr
    and Expr
    p Expr
    q = Ident -> [Expr] -> Expr
    app Ident
    "and" [Expr
    p,Expr
    q]

    or :: Expr -> Expr -> Expr
    or :: Expr -> Expr -> Expr
    or Expr
    p Expr
    q = Ident -> [Expr] -> Expr
    app Ident
    "or" [Expr
    p,Expr
    q]

    xor :: Expr -> Expr -> Expr
    xor :: Expr -> Expr -> Expr
    xor Expr
    p Expr
    q = Ident -> [Expr] -> Expr
    app Ident
    "xor" [Expr
    p,Expr
    q]

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

    (=/=) :: Expr -> Expr -> Expr
    Expr
    x =/= :: Expr -> Expr -> Expr
    =/= Expr
    y = Ident -> [Expr] -> Expr
    app Ident
    "distinct" [Expr
    x,Expr
    y]

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