mathlib documentation

meta def old_conv (α : Type) :

meta def old_conv.lhs  :

meta def old_conv.change (new_p : pexpr) :

meta def old_conv.pure {α : Type} :

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 β) :

meta def old_conv.monad  :

meta def old_conv.alternative  :

meta def old_conv.whnf (md : tactic.transparency := reducible) :

meta def old_conv.dsimp  :

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

meta def old_conv.trace_lhs  :

meta def old_conv.apply_lemmas_core (s : simp_lemmas) (prove : tactic unit) :

meta def old_conv.apply_lemmas (s : simp_lemmas) :

meta def old_conv.apply_propext_lemmas_core (s : simp_lemmas) (prove : tactic unit) :

meta def old_conv.apply_propext_lemmas (s : simp_lemmas) :

meta def old_conv.to_tactic (c : old_conv unit) :

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

meta def old_conv.apply_simp_set (attr_name : name) :

meta def old_conv.apply_propext_simp_set (attr_name : name) :

meta def old_conv.skip  :

meta def old_conv.repeat  :

meta def old_conv.first {α : Type} :

meta def old_conv.match_pattern (p : tactic.pattern) :

meta def old_conv.mk_match_expr (p : pexpr) :

meta def old_conv.match_expr (p : pexpr) :

meta def old_conv.funext (c : old_conv unit) :

meta def old_conv.congr_core (c_f c_a : old_conv unit) :

meta def old_conv.congr (c : old_conv unit) :

meta def old_conv.bottom_up (c : old_conv unit) :

meta def old_conv.top_down (c : old_conv unit) :

meta def old_conv.find (c : old_conv unit) :

meta def old_conv.find_pattern (pat : tactic.pattern) (c : old_conv unit) :

meta def old_conv.findp  :

meta def old_conv.conversion (c : old_conv unit) :