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