mathlib docs: tactic.omega.misc

theorem omega.fun_mono_2 {α β γ : Type} {p : α → β → γ} {a1 a2 : α} {b1 b2 : β} (a : a1 = a2) (a_1 : b1 = b2) :

p a1 b1 = p a2 b2

theorem omega.pred_mono_2 {α β : Type} {p : α → β → Prop} {a1 a2 : α} {b1 b2 : β} (a : a1 = a2) (a_1 : b1 = b2) :

p a1 b1 ↔ p a2 b2

theorem omega.pred_mono_2' {c : Prop → Prop → Prop} {a1 a2 b1 b2 : Prop} (a : a1 ↔ a2) (a_1 : b1 ↔ b2) :

c a1 b1 ↔ c a2 b2

def omega.update {α : Type} (m : ℕ) (a : α) (v : ℕ → α) (a_1 : ℕ) :

α

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

Equations

theorem omega.update_eq {α : Type} (m : ℕ) (a : α) (v : ℕ → α) :

v ⟨m ↦ a⟩ m = a

theorem omega.update_eq_of_ne {α : Type} {m : ℕ} {a : α} {v : ℕ → α} (k : ℕ) (a_1 : k ≠ m) :

v ⟨m ↦ a⟩ k = v k

def omega.update_zero {α : Type} (a : α) (v : ℕ → α) (a_1 : ℕ) :

α

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

Equations

meta def omega.intro_fresh :

Intro with a fresh name

meta def omega.revert_cond (t : expr → tactic unit) (x : expr) :

Revert an expr if it passes the given test

meta def omega.revert_cond_all (t : expr → tactic unit) :

Revert all exprs in the context that pass the given test

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

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