free_vars

proveit.free_vars(expr)

Returns the set of variables for that are free (unbound) in the given expression. For example, given

(x_1, …, x_n) -> x_1 + … + x_{m}

n is free. Even though there is ambiguity about the range of indices of x on the right versus the left without knowing m relative to n, lambda maps in Prove-It are not allowed to partially mask a range of parameters (in this example, m>n is not allowed). However, this restriction isn’t enforced until it really matters. When the ranges of x are relabeled or instantiated, then Prove-It will check that this restriction is satisfied. Axioms and theorems must not have any variables that are entirely free.