meta def tactic.intro : name → tactic expr :=
λ (n : name),
  id_rhs (tactic expr)
    (tactic.target >>=
       λ (t : expr),
         ite (↥(expr.is_pi t) ∨ ↥(expr.is_let t)) (tactic.intro_core n)
           (tactic.whnf_target >> tactic.intro_core n))
