mathlib documentation

tactic.converter.old_conv

meta structure old_conv_result (α : Type) :
Type

meta def old_conv (α : Type) :
Type

meta def old_conv.change (new_p : pexpr) :

meta def old_conv.pure {α : Type} :
α → old_conv α

meta def old_conv.seq {α β : Type} (c₁ : old_conv (α → β)) (c₂ : old_conv α) :

meta def old_conv.fail {α β : Type} [has_to_format β] (msg : β) :

meta def old_conv.failed {α : Type} :

meta def old_conv.orelse {α : Type} (c₁ c₂ : old_conv α) :

meta def old_conv.map {α β : Type} (f : α → β) (c : old_conv α) :

meta def old_conv.bind {α β : Type} (c₁ : old_conv α) (c₂ : α → old_conv β) :

@[instance]

@[instance]

meta def old_conv.trace {α : Type} [has_to_tactic_format α] (a : α) :

meta def old_conv.lift_tactic {α : Type} (t : tactic α) :

meta def old_conv.apply_simp_set (attr_name : name) :

meta def old_conv.first {α : Type} :
list (old_conv α)old_conv α