mk_type_variable method

Z3_sort mk_type_variable(
  1. Z3_context c,
  2. Z3_symbol s
)

\brief Create a type variable.

Functions using type variables can be applied to instantiations that match the signature of the function. Assertions using type variables correspond to assertions over all possible instantiations.

def_API('Z3_mk_type_variable', SORT, (_in(CONTEXT), _in(SYMBOL)))

Implementation

Z3_sort mk_type_variable(
  Z3_context c,
  Z3_symbol s,
) {
  return _mk_type_variable(
    c,
    s,
  );
}