parameters: (ctx=None)
return_statement: return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
docstring: Return the integer sort in the given context. If `ctx=None`, then the global context is used.
  
      >>> IntSort()
      Int
      >>> x = Const('x', IntSort())
      >>> is_int(x)
      True
      >>> x.sort() == IntSort()
      True
      >>> x.sort() == BoolSort()
      False
docstring_summary: Return the integer sort in the given context. If `ctx=None`, then the global context is used.
docstring_tokens: Return the integer sort in the given context . If ctx = None then the global context is used .
function: def IntSort(ctx=None):
      """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
  
      >>> IntSort()
      Int
      >>> x = Const('x', IntSort())
      >>> is_int(x)
      True
      >>> x.sort() == IntSort()
      True
      >>> x.sort() == BoolSort()
      False
      """
      ctx = _get_ctx(ctx)
      return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
function_tokens: def IntSort ( ctx = None ) : ctx = _get_ctx ( ctx ) return ArithSortRef ( Z3_mk_int_sort ( ctx . ref ( ) ) , ctx )