Stream: Beginner Questions

Topic: Using let-defined names in structured proofs


view this post on Zulip Yong Kiam (Jun 18 2024 at 07:45):

This is somewhat vague question... when defining an algorithm, one might typically write a number of lets:

definition foo where "foo x = let y = f x in z = g y in ..."

in a structured proof of this, I often find myself wanting to refer to that same structure and writing:

proof -
define y where "y = f x"
define z where "z = g y"
...

my question: is there a better way of doing this?


Last updated: Dec 21 2024 at 16:20 UTC