Skip to main content

mk_var

cvc5_sys

Function mk_var 

Source 
pub unsafe extern "C" fn mk_var(
    tm: *mut TermManager,
    sort: Sort,
    symbol: *const c_char,
) -> Term
Expand description

Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder). @param tm The term manager instance. @param sort The sort of the variable. @param symbol The name of the variable, may be NULL. @return The variable.