Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: rw / clear - ident?


view this post on Zulip Henning Dieterichs (Jan 05 2021 at 22:13):

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?

view this post on Zulip Yakov Pechersky (Jan 05 2021 at 22:18):

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

view this post on Zulip Henning Dieterichs (Jan 05 2021 at 22:29):

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

view this post on Zulip Henning Dieterichs (Jan 05 2021 at 22:41):

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

view this post on Zulip Henning Dieterichs (Jan 06 2021 at 10:36):

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

view this post on Zulip Jannis Limperg (Jan 06 2021 at 10:45):

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.

view this post on Zulip Jannis Limperg (Jan 06 2021 at 10:46):

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.

view this post on Zulip Henning Dieterichs (Jan 06 2021 at 11:16):

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.

view this post on Zulip Jannis Limperg (Jan 06 2021 at 11:17):

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

view this post on Zulip Henning Dieterichs (Jan 06 2021 at 11:21):

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


Last updated: May 09 2021 at 22:13 UTC