Zulip Chat Archive

Stream: general

Topic: Show partial proof term in the proof mode


Mingzhe Wang (Mar 10 2022 at 19:09):

I am new to Lean. I know we can print the proof term after proving a lemma. Is there a way to display the partial proof term when we are writing the proof, like the command "Show Proof" in coq?

Gabriel Ebner (Mar 10 2022 at 19:10):

There's the show_term tactic. https://leanprover-community.github.io/mathlib_docs/tactics.html#show_term

Mingzhe Wang (Mar 10 2022 at 19:13):

Thanks Gabriel! This is really helpful!


Last updated: Aug 03 2023 at 10:10 UTC