Zulip Chat Archive

Stream: new members

Topic: Help with proof terms

Vivek Rajesh Joshi (Aug 17 2023 at 09:21):

I have been practicing lean for a while now, and I'm getting comfortable with the tactic-style proofs. But whenever I encounter a proof term, it throws me off balance. I'm unable to grasp them despite looking at several examples of them. Could someone please explain to me how to use and understand proof terms, or direct me to a source that does so?

Ioannis Konstantoulas (Aug 17 2023 at 10:01):

The book Theorem Proving in Lean 4 explains and makes heavy use of proof terms in the first chapters.

Last updated: Dec 20 2023 at 11:08 UTC