Stream: Beginner Questions

Topic: Prevent safe from splitting tuples

view this post on Zulip MackieLoeffel (Mar 26 2024 at 10:23):

Hi, is there a way to prevent safe from destructing universally quantified tuples?

In particular, I would like safe to not do anything on the following goal:

lemma test : "⋀ (a :: (_ * _)). P a"
  apply (safe)

but it transforms the goal into ⋀a b. P (a, b). Is there a way to prevent this?

Last updated: Apr 27 2024 at 20:14 UTC