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?
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?
@Wolfgang Jeltsch but that's the point, I do not have an argument there, only the function.
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
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?
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
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: Dec 07 2023 at 08:19 UTC