sig
  val mk_sort :
    Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.Sort.sort
  val mk_list_s : Z3.context -> string -> Z3.Sort.sort -> Z3.Sort.sort
  val get_nil_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val get_is_nil_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val get_cons_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val get_is_cons_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val get_head_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val get_tail_decl : Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val nil : Z3.Sort.sort -> Z3.Expr.expr
end