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} (a : α) :

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.to_tactic (c : old_conv unit) (a : name) (a_1 : expr) :

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} (a : list (old_conv α)) :

meta def old_conv.findp (a : pexpr) (a_1 : old_conv unit) :