sig
  type token =
      TRUE
    | RIGHT_PAREN
    | RESULT_VAL
    | RESULT_UNSAT
    | RESULT_UNKNOWN
    | RESULT_TYPE
    | RESULT_TIMEOUT
    | RESULT_SAT
    | RESULT_RESULT
    | RESULT_MODEL
    | QUOTED of string
    | PAR
    | OR
    | NOT
    | MATCH
    | LET
    | LEFT_PAREN
    | IF
    | IDENT of string
    | FUN
    | FORALL
    | FALSE
    | EXISTS
    | EQ
    | EOI
    | DEFINE_FUN_REC
    | DEFINE_FUNS_REC
    | DEFINE_FUN
    | DEFAULT
    | DECLARE_SORT
    | DECLARE_FUN
    | DECLARE_CONST
    | DATA
    | CHECK_SAT
    | CASE
    | BOOL
    | AT
    | ASSERT_NOT
    | ASSERT
    | AS
    | ARROW
    | AND
  exception Error
  val parse_ty :
    (Lexing.lexbuf -> Tip_parser.token) -> Lexing.lexbuf -> Tip_ast.ty
  val parse_term :
    (Lexing.lexbuf -> Tip_parser.token) -> Lexing.lexbuf -> Tip_ast.term
  val parse_smbc_res :
    (Lexing.lexbuf -> Tip_parser.token) ->
    Lexing.lexbuf -> Tip_ast.Smbc_res.t
  val parse_list :
    (Lexing.lexbuf -> Tip_parser.token) ->
    Lexing.lexbuf -> Tip_ast.statement list
  val parse :
    (Lexing.lexbuf -> Tip_parser.token) -> Lexing.lexbuf -> Tip_ast.statement
end