Gergely Buday (Sep 20 2023 at 10:23): Gergely Buday (Sep 20 2023 at 10:23):I have a datatype along the lines of
datatype 'a dummy = Foo 'a | Bar 'a => 'a dummy
Is it possible to do a case distinction on whether a Bar value's function returns a Foo or a Bar?
Wolfgang Jeltsch (Sep 20 2023 at 10:56):I fear I don’t fully understand what you mean. For a case distinction you would need a fixed argument for the function under Bar, I’d say. Could you please clarify?
Gergely Buday (Sep 20 2023 at 11:56):@Wolfgang Jeltsch but that's the point, I do not have an argument there, only the function.
Yong Kiam (Sep 20 2023 at 14:29):I agree with @Wolfgang Jeltsch this doesn't seem like a well-formed question:
If I have a Bar f, the function f can return either Foo or another Bar depending on its input
Wolfgang Jeltsch (Sep 20 2023 at 15:03):Gergely Buday said:
Wolfgang Jeltsch but that's the point, I do not have an argument there, only the function.
But what exactly do you want to do?
Wolfgang Jeltsch (Sep 20 2023 at 15:07):Case distinction is about having different subproofs of different kinds of values that some variable can take. For example, if your variable is of type nat, you can distinguish between the cases 0 and Suc _. But what should your cases for 'a ⇒ 'a dummy be? There are functions in this type that return only Foo values, others that return only Bar values, yet others that return Foo values for some arguments and Barvalues for others according to whatever patterns.
Last updated: May 01 2024 at 20:18 UTC