Bernhard Stöckl (Sep 20 2021 at 14:07): Bernhard Stöckl (Sep 20 2021 at 14:07):I'm trying to use a recursive datatype that uses sets like this:
datatype 'a test = Test 'a "('a test) set"
But this results in the error
Unsupported recursive occurrence of type "'a test" via type constructor "Set.set" in type expression "'a test set"
Use the "bnf" command to register "Set.set" as a bounded natural functor to allow nested (co)recursion through it
If I use "list" or "fset" instead of "set" it works. But is there a way to do this with normal sets or should I just use fsets instead?
Dmitriy Traytel (Sep 20 2021 at 16:11):If this was allowed, Test x :: 'a test set => 'a test would be a total, injective function from the the powerset of a set to the set. You could prove False from that easily.
The BNF abstraction is what separates types that may nest recursive occurrences from those which may not. The types of lists and finite sets are BNFs, but "'a set" isn't.
Bernhard Stöckl (Sep 20 2021 at 16:30):Ok, thanks for the explanation :smile:
Notification Bot (Sep 20 2021 at 16:30):Bernhard Stöckl has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC