rw / clear - ident?

Stream: metaprogramming / tactics

[Henning Dieterichs]

I'm trying to define an inline tactic:

import tactic

open tactic expr

namespace tactic
namespace interactive
setup_tactic_parser

meta def inline (h : parse ident): tactic unit :=
    `[
        rw [%%h] at *,
        clear %%h
    ]

end interactive
end tactic

I get the error invalid antiquotation, occurs outside of quoted expressions at clear though. I don't understand that error.
How can I fix that?

[Yakov Pechersky]

I think this tactic already exists, and is called "subst"

[Henning Dieterichs]

Thanks! Missed it. But I'm still interesting in why my inline tactic does not type-check!

[Henning Dieterichs]

Well, subst does only work for x = t or t = x. Not for t = t!

[Henning Dieterichs]

meta def inline (h : parse parser.pexpr): tactic unit :=
do
    m ← match_local_const h,
    trace (expr.to_raw_fmt h),
        rewrite
            { rules:= [{pos := {line := 43, column := 11}, symm := ff, rule := h}], end_pos:=none }
            loc.wildcard,
        tactic.clear_lst [m.fst]

This works! It would be great if rewrite would not change the order of the hypothesis though

[Jannis Limperg]

This is an unfortunate aspect of Lean metaprogramming: many tactics are implemented as revert <hyps>, <something>, intros, which doesn't always preserve the order of hypotheses. If this is important to you, I'm sure people would welcome a fix, but it's not going to be super easy.

[Jannis Limperg]

If you're going to do more metaprogramming, you might be interested in a blog post of mine where I talk about some more of Lean's gotchas.

[Henning Dieterichs]

Thank you for the link! While I would love to be fluent in metaprogramming, I find it way too complex and difficult to learn with the current tools at hand. Keeping the order of hyps is not super important for me, it is nice that it works at all.

[Jannis Limperg]

Fair enough. It took me the better part of a year to get the hang of it, so I feel you. ;)

[Henning Dieterichs]

I really like leans dot-notation and the autocompletion it offers (at least most of the time). However, as soon as you need a random undocumented function in some obscure namespace it is just trail&error and guessing for me. I found it way easier to extend and play around with the internals of the typescript language service. It is very nice though that you don't need to wait for any compilation in lean. I miss a debugger nonetheless :D