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?
Reid Barton (Sep 08 2018 at 00:26):
oh, I made something that kind of works! Never mind
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