Stream: General

Topic: (How) can I declare a domain a codatatype (or vice-versa)?

view this post on Zulip Max Baumann (Feb 26 2024 at 09:51):

I have a domain declared somewhat like this:

domain ('a :: "domain") llist = LCons (lhd::"'a") (lazy ltl::"'a llist")

Can I additionally make this a codatatype, like this?

codatatype 'a llist = lbot:LNil | LCons(lhd:'a) (ltl:"'a llist")

view this post on Zulip Manuel Eberl (Feb 26 2024 at 14:45):

What is a "domain"? Are you using some special package?

view this post on Zulip Max Baumann (Feb 26 2024 at 14:50):

Sorry, forgot to mention it. It's a HOLCF domain.

Last updated: Dec 21 2024 at 16:20 UTC