mathlib docs: tactic.converter.binders

source

@[instance]

meta def old_conv.monad_fail :

monad_fail old_conv

source

@[instance]

meta def old_conv.has_monad_lift :

has_monad_lift tactic old_conv

source

@[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 :

expr → list (list expr → old_conv unit) → old_conv unit

source

meta def old_conv.congr_binder :

name → (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} :

old_conv α → old_conv α

source

meta def old_conv.apply :

expr → old_conv unit

source

meta def old_conv.applyc :

name → old_conv unit

source

meta def old_conv.apply' :

name → old_conv unit

source

meta structure binder_eq_elim :

Type

match_binder : expr → tactic (expr × expr)
adapt_rel : old_conv unit → old_conv unit
apply_comm : old_conv unit
apply_congr : (expr → old_conv unit) → old_conv unit
apply_elim_eq : old_conv unit

source

meta def binder_eq_elim.check_eq :

binder_eq_elim → expr → expr → tactic unit

source

meta def binder_eq_elim.pull :

binder_eq_elim → expr → old_conv unit

source

meta def binder_eq_elim.push :

binder_eq_elim → old_conv unit

source

meta def binder_eq_elim.check :

binder_eq_elim → expr → expr → tactic unit

source

meta def binder_eq_elim.old_conv :

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

mathlib documentation

tactic.converter.binders

General documentation

Additional documentation

Library

mathlib documentation

tactic.​converter.​binders

General documentation

Additional documentation

Library

tactic.converter.binders