Stream: Coq users

Topic: ✔ Define Polymorphic Datatype

view this post on Zulip Jiahong Lee (Jun 02 2022 at 08:32):

Théo Winterhalter said:

The second is the way to go I think, but it also makes the parameters implicit in the type, you can add the line

Arguments result2 _ _ : clear implicits.

to fix it.

Thanks, this works!

view this post on Zulip Jiahong Lee (Jun 02 2022 at 08:33):

Regarding the extra _, for Ok it corresponds to the x : OkType.

Ah, makes sense, only now then I realise every result constructors takes two extra arguments due to the polymorphic declaration.

view this post on Zulip Jiahong Lee (Jun 02 2022 at 08:39):

Arguments can work on a prefix of the arguments (thankfully because there is no distinction between a function with one argument returning a function and a function with two arguments).

I see, I thought that holds for every command due to function currying? Not sure, I'm just getting started

view this post on Zulip Notification Bot (Jun 02 2022 at 08:40):

Jiahong Lee has marked this topic as resolved.

Last updated: Jan 27 2023 at 02:04 UTC