mathlib3 documentation

tactic.converter.binders

source
@[protected, instance]
meta def old_conv.monad_fail  :
monad_fail old_conv
source
@[protected, instance]
meta def old_conv.has_monad_lift  :
has_monad_lift tactic old_conv
source
@[protected, instance]
meta def old_conv.has_coe (α : Type) :
has_coe (tactic α) (old_conv α)
source
meta def old_conv.current_relation  :
old_conv name
source
meta def old_conv.head_beta  :
old_conv unit
source
meta def old_conv.congr_arg  :
old_conv unit → old_conv unit
source
meta def old_conv.congr_fun  :
old_conv unit → old_conv unit
source
meta def old_conv.congr_rule (congr : expr) (cs : list (list expr → old_conv unit)) :
old_conv unit
source
meta def old_conv.congr_binder (congr : name) (cs : expr → old_conv unit) :
old_conv unit
source
meta def old_conv.funext'  :
(expr → old_conv unit) → old_conv unit
source
meta def old_conv.propext' {α : Type} (c : old_conv α) :
old_conv α
source
meta def old_conv.apply (pr : expr) :
old_conv unit
source
meta def old_conv.applyc (n : name) :
old_conv unit
source
meta def old_conv.apply' (n : name) :
old_conv unit
source
meta structure binder_eq_elim  :
Type
source
meta def binder_eq_elim.check_eq (b : binder_eq_elim) (x : expr) :
expr → tactic unit
source
meta def binder_eq_elim.pull (b : binder_eq_elim) (x : expr) :
old_conv unit
source
meta def binder_eq_elim.push (b : binder_eq_elim) :
old_conv unit
source
meta def binder_eq_elim.check (b : binder_eq_elim) (x : expr) :
expr → tactic unit
source
meta def binder_eq_elim.old_conv (b : binder_eq_elim) :
old_conv unit
source
theorem exists_elim_eq_left {α : Sort u} (a : α) (p : Π (a' : α), a' = a → Prop) :
(∃ (a' : α) (h : a' = a), p a' h) ↔ p a rfl
source
theorem exists_elim_eq_right {α : Sort u} (a : α) (p : Π (a' : α), a = a' → Prop) :
(∃ (a' : α) (h : a = a'), p a' h) ↔ p a rfl
source
meta def exists_eq_elim  :
binder_eq_elim
source
theorem forall_comm {α : Sort u} {β : Sort v} (p : α → β → Prop) :
(∀ (a : α) (b : β), p a b) ↔ ∀ (b : β) (a : α), p a b
source
theorem forall_elim_eq_left {α : Sort u} (a : α) (p : Π (a' : α), a' = a → Prop) :
(∀ (a' : α) (h : a' = a), p a' h) ↔ p a rfl
source
theorem forall_elim_eq_right {α : Sort u} (a : α) (p : Π (a' : α), a = a' → Prop) :
(∀ (a' : α) (h : a = a'), p a' h) ↔ p a rfl
source
meta def forall_eq_elim  :
binder_eq_elim
source
meta def supr_eq_elim  :
binder_eq_elim
source
meta def infi_eq_elim  :
binder_eq_elim