Max Baumann (Jan 16 2024 at 08:49): Max Baumann (Jan 16 2024 at 08:49):Hi! I ran into this error:
Wellsortedness error:
Type nat not of sort enum
No type arity nat :: enum
How do I go about debugging this?
Can I let Isabelle tell me why it requires nat to be enum?
This happens when attempting to run quickcheck
Maximilian Schäffeler (Jan 16 2024 at 11:54):The type class enum requires a finitely enumerable type. Since nat is not finite, there cannot be an instance nat :: enum. Some of your definitions that quickcheck tries to evaluate require an enumerable type. Only then they are executable, e.g. try value {x :: nat. x < 3}. You may be able to prove code equations to resolve this issue, e.g. value {..<3::nat} works and produces the desired result. However, I would need more information about your definitions to really help you with that.
Max Baumann (Jan 16 2024 at 12:12):Yes, I hoped to see why Isabelle wants nat to be enum.
Maximilian Schäffeler (Jan 17 2024 at 13:27):To be able to generate code (to execute quickcheck, I think), but that's only needed for some constructs. That's why I asked for more information about your definition :)
Last updated: Dec 21 2024 at 16:20 UTC