mathlib documentation

tactic.converter.binders

@[instance]
@[instance]
meta def old_conv.has_coe (α : Type) :
meta def old_conv.congr_rule (congr : expr) (cs : list (list exprold_conv unit)) :
meta def old_conv.congr_binder (congr : name) (cs : exprold_conv unit) :
meta def old_conv.propext' {α : Type} (c : old_conv α) :
meta def old_conv.apply (pr : expr) :
meta structure binder_eq_elim  :
Type
theorem exists_elim_eq_left {α : Sort u} (a : α) (p : Π (a' : α), a' = a → Prop) :
(∃ (a' : α) (h : a' = a), p a' h) p a rfl
theorem exists_elim_eq_right {α : Sort u} (a : α) (p : Π (a' : α), a = a' → Prop) :
(∃ (a' : α) (h : a = a'), p a' h) p a rfl
theorem forall_comm {α : Sort u} {β : Sort v} (p : α → β → Prop) :
(∀ (a : α) (b : β), p a b) ∀ (b : β) (a : α), p a b
theorem forall_elim_eq_left {α : Sort u} (a : α) (p : Π (a' : α), a' = a → Prop) :
(∀ (a' : α) (h : a' = a), p a' h) p a rfl
theorem forall_elim_eq_right {α : Sort u} (a : α) (p : Π (a' : α), a = a' → Prop) :
(∀ (a' : α) (h : a = a'), p a' h) p a rfl