mathlib3 documentation

tactic.converter.old_conv

meta structure old_conv_result (α : Type) :
meta def old_conv (α : Type) :
Instances for old_conv
meta def old_conv.change (new_p : pexpr) :
@[protected]
meta def old_conv.pure {α : Type} :
@[protected]
meta def old_conv.seq {α β : Type} (c₁ : old_conv β)) (c₂ : old_conv α) :
@[protected]
meta def old_conv.fail {α β : Type} [has_to_format β] (msg : β) :
@[protected]
meta def old_conv.failed {α : Type} :
@[protected]
meta def old_conv.orelse {α : Type} (c₁ c₂ : old_conv α) :
@[protected]
meta def old_conv.map {α β : Type} (f : α β) (c : old_conv α) :
@[protected]
meta def old_conv.bind {α β : Type} (c₁ : old_conv α) (c₂ : α old_conv β) :
@[protected, instance]
@[protected, 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} :