Zulip Chat Archive

Stream: general

Topic: metavars


view this post on Zulip Reid Barton (Sep 08 2018 at 00:16):

This is probably a confused question, but in a tactic, how do I create a metavariable that can potentially depend on other metavariables?

view this post on Zulip Reid Barton (Sep 08 2018 at 00:26):

oh, I made something that kind of works! Never mind

view this post on Zulip Sebastien Gouezel (Jun 27 2020 at 07:40):

I have a proof in which an exact takes avery long time. The reason, I guess, is that in the goal there is a metavar (or, more precisely, one can see the metavar if one uses pp.instantiate_mvars false, but otherwise the metavar is replaced by its value, so Lean knows exactly what it should be). Is there a command to instantiate the metavar, to see if it makes the proof faster?

(The metavar is coming from a convert. If it could clean up the mess for me, it would be even better!)


Last updated: May 10 2021 at 18:22 UTC