mathlib documentation

tactic.converter.old_conv

meta structure old_conv_result  :
Type → Type

meta def old_conv  :
Type → Type

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

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

meta def old_conv.fail {α β : Type} [has_to_format β] :
β → old_conv α

meta def old_conv.failed {α : Type} :

meta def old_conv.orelse {α : Type} :
old_conv αold_conv αold_conv α

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

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

@[instance]

@[instance]

meta def old_conv.trace {α : Type} [has_to_tactic_format α] :
α → old_conv unit

meta def old_conv.lift_tactic {α : Type} :
tactic αold_conv α

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