Zulip Chat Archive

Stream: lean4

Topic: squeeze_simp

Horatiu Cheval (Nov 10 2021 at 21:20):

Is there a Lean4 version of squeeze_simp? I can't find it at the moment. Or any other way of replacing nonterminal simps with the appropriate simp only?

Scott Morrison (Nov 10 2021 at 22:13):

No, not yet. In the meantime you could showTerm simp and interpret the output yourself to extract the lemma names. It won't be pretty.

Last updated: Dec 20 2023 at 11:08 UTC