Update variable assignment for a specific variable and leave everything else unchanged
Equations
- omega.update m a v n = ite (n = m) a (v n)
theorem
omega.update_eq_of_ne
{α : Type}
{m : ℕ}
{a : α}
{v : ℕ → α}
(k : ℕ) :
k ≠ m → omega.update m a v k = v k
Assign a new value to the zeroth variable, and push all other assignments up by 1
Equations
- omega.update_zero a v (k + 1) = v k
- omega.update_zero a v 0 = a
Try applying a tactic to each of the element in a list until success, and return the first successful result