Stream: math-comp users

Topic: ✔ Empty finType

view this post on Zulip 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.

view this post on Zulip Notification Bot (Nov 14 2022 at 00:20):

Ricardo has marked this topic as resolved.

Last updated: Jan 29 2023 at 19:02 UTC