Jason Gross (Mar 06 2021 at 16:32):
I have a hole where Lean says "don't know how to synthesize placeholder" and lists a bunch of things in the context. I want to run the equivalent of Coq's
simpl tactic in the context and see the result. (I'd be willing to explicitly name the things I want to unfold if that's better, and, in this case, I'd also be fine with fully normalizing everything). How do I do this?
Leonardo de Moura (Mar 06 2021 at 16:55):
Have you tried to use tactic mode? Suppose you have a hole
_ that cannot be synthesized, you can replace it with
(by done), where
done is a tactic that fails when there are unsolved goals. Then, you can use tactics to simplify the context.
(by clear h; simp; done). Note that
simp is not Coq
simpl since it will use theorems marked with
[simp] as rewriting rules, but you can use
simp only instead. Btw,
simp only [foo] unfolds
simp only [foo] at h unfolds
foo at hypothesis
Jason Gross (Mar 08 2021 at 14:11):
I'm now trying this out; thanks!
Last updated: May 07 2021 at 13:21 UTC