parameters: (a)
return_statement: return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
docstring: Return `True` if `a` is variable.
  
      Z3 uses de-Bruijn indices for representing bound variables in
      quantifiers.
  
      >>> x = Int('x')
      >>> is_var(x)
      False
      >>> is_const(x)
      True
      >>> f = Function('f', IntSort(), IntSort())
      >>> # Z3 replaces x with bound variables when ForAll is executed.
      >>> q = ForAll(x, f(x) == x)
      >>> b = q.body()
      >>> b
      f(Var(0)) == Var(0)
      >>> b.arg(1)
      Var(0)
      >>> is_var(b.arg(1))
      True
docstring_summary: Return `True` if `a` is variable.
docstring_tokens: Return True if a is variable .
function: def is_var(a):
      """Return `True` if `a` is variable.
  
      Z3 uses de-Bruijn indices for representing bound variables in
      quantifiers.
  
      >>> x = Int('x')
      >>> is_var(x)
      False
      >>> is_const(x)
      True
      >>> f = Function('f', IntSort(), IntSort())
      >>> # Z3 replaces x with bound variables when ForAll is executed.
      >>> q = ForAll(x, f(x) == x)
      >>> b = q.body()
      >>> b
      f(Var(0)) == Var(0)
      >>> b.arg(1)
      Var(0)
      >>> is_var(b.arg(1))
      True
      """
      return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
function_tokens: def is_var ( a ) : return is_expr ( a ) and _ast_kind ( a . ctx , a ) == Z3_VAR_AST