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!
Regarding the extra
_
, forOk
it corresponds to thex : OkType
.
Ah, makes sense, only now then I realise every result
constructors takes two extra arguments due to the polymorphic declaration.
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
Jiahong Lee has marked this topic as resolved.
Last updated: Jan 27 2023 at 02:04 UTC