Ricardo (Nov 14 2022 at 00:20): Ricardo (Nov 14 2022 at 00:20):I see. Thank you Ana and Paolo. I thought about how to use a function taking {T : choiceType} (x : T) to be able to write sg nat nat. Since a particular nat value has to be given to the function for it to recreate T, I don't think it's possible. I came up with this simple notation instead.
Notation sgn := (sg [choiceType of nat] [choiceType of nat]).
I think that'll be enough for now. Thank you.
Notification Bot (Nov 14 2022 at 00:20):Ricardo has marked this topic as resolved.
Last updated: Jan 29 2023 at 19:02 UTC