mathlib3 documentation

tactic.converter.old_conv

source
meta structure old_conv_result (α : Type) :
Type
source
meta def old_conv (α : Type) :
Type
Instances for old_conv
source
meta def old_conv.lhs  :
old_conv expr
source
meta def old_conv.change (new_p : pexpr) :
old_conv unit
source
@[protected]
meta def old_conv.pure {α : Type} :
α → old_conv α
source
@[protected]
meta def old_conv.seq {α β : Type} (c₁ : old_conv (α → β)) (c₂ : old_conv α) :
old_conv β
source
@[protected]
meta def old_conv.fail {α β : Type} [has_to_format β] (msg : β) :
old_conv α
source
@[protected]
meta def old_conv.failed {α : Type} :
old_conv α
source
@[protected]
meta def old_conv.orelse {α : Type} (c₁ c₂ : old_conv α) :
old_conv α
source
@[protected]
meta def old_conv.map {α β : Type} (f : α → β) (c : old_conv α) :
old_conv β
source
@[protected]
meta def old_conv.bind {α β : Type} (c₁ : old_conv α) (c₂ : α → old_conv β) :
old_conv β
source
@[protected, instance]
meta def old_conv.monad  :
monad old_conv
source
@[protected, instance]
meta def old_conv.alternative  :
alternative old_conv
source
meta def old_conv.whnf (md : tactic.transparency := tactic.transparency.reducible) :
old_conv unit
source
meta def old_conv.dsimp  :
old_conv unit
source
meta def old_conv.trace {α : Type} [has_to_tactic_format α] (a : α) :
old_conv unit
source
meta def old_conv.trace_lhs  :
old_conv unit
source
meta def old_conv.apply_lemmas_core (s : simp_lemmas) (prove : tactic unit) :
old_conv unit
source
meta def old_conv.apply_lemmas (s : simp_lemmas) :
old_conv unit
source
meta def old_conv.apply_propext_lemmas_core (s : simp_lemmas) (prove : tactic unit) :
old_conv unit
source
meta def old_conv.apply_propext_lemmas (s : simp_lemmas) :
old_conv unit
source
meta def old_conv.to_tactic (c : old_conv unit) :
name → expr → tactic (expr × expr)
source
meta def old_conv.lift_tactic {α : Type} (t : tactic α) :
old_conv α
source
meta def old_conv.apply_simp_set (attr_name : name) :
old_conv unit
source
meta def old_conv.apply_propext_simp_set (attr_name : name) :
old_conv unit
source
meta def old_conv.skip  :
old_conv unit
source
meta def old_conv.repeat  :
old_conv unit → old_conv unit
source
meta def old_conv.first {α : Type} :
list (old_conv α) → old_conv α
source
meta def old_conv.match_pattern (p : tactic.pattern) :
old_conv unit
source
meta def old_conv.mk_match_expr (p : pexpr) :
tactic (old_conv unit)
source
meta def old_conv.match_expr (p : pexpr) :
old_conv unit
source
meta def old_conv.funext (c : old_conv unit) :
old_conv unit
source
meta def old_conv.congr_core (c_f c_a : old_conv unit) :
old_conv unit
source
meta def old_conv.congr (c : old_conv unit) :
old_conv unit
source
meta def old_conv.bottom_up (c : old_conv unit) :
old_conv unit
source
meta def old_conv.top_down (c : old_conv unit) :
old_conv unit
source
meta def old_conv.find (c : old_conv unit) :
old_conv unit
source
meta def old_conv.find_pattern (pat : tactic.pattern) (c : old_conv unit) :
old_conv unit
source
meta def old_conv.findp  :
pexpr → old_conv unit → old_conv unit
source
meta def old_conv.conversion (c : old_conv unit) :
tactic unit