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

    import SMTLib2.AST

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

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

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

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

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

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

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

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

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

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

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