# mathlib3documentation

tactic.omega.misc

theorem omega.fun_mono_2 {α β γ : Type} {p : α β γ} {a1 a2 : α} {b1 b2 : β} :
a1 = a2 b1 = b2 p a1 b1 = p a2 b2
theorem omega.pred_mono_2 {α β : Type} {p : α β Prop} {a1 a2 : α} {b1 b2 : β} :
a1 = a2 b1 = b2 (p a1 b1 p a2 b2)
theorem omega.pred_mono_2' {c : Prop Prop Prop} {a1 a2 b1 b2 : Prop} :
(a1 a2) (b1 b2) (c a1 b1 c a2 b2)
def omega.update {α : Type} (m : ) (a : α) (v : α) :
α

Update variable assignment for a specific variable and leave everything else unchanged

Equations
• a v n = ite (n = m) a (v n)
theorem omega.update_eq {α : Type} (m : ) (a : α) (v : α) :
a v m = a
theorem omega.update_eq_of_ne {α : Type} {m : } {a : α} {v : α} (k : ) :
k m a v k = v k
def omega.update_zero {α : Type} (a : α) (v : α) :
α

Assign a new value to the zeroth variable, and push all other assignments up by 1

Equations
• (k + 1) = v k
• 0 = a
meta def omega.intro_fresh  :

Intro with a fresh name

meta def omega.revert_cond (t : expr ) (x : expr) :

Revert an expr if it passes the given test

meta def omega.revert_cond_all (t : expr ) :

Revert all exprs in the context that pass the given test

meta def omega.app_first {α β : Type} (t : α ) :
list α

Try applying a tactic to each of the element in a list until success, and return the first successful result