Zulip Chat Archive
Stream: Is there code for X?
Topic: fin.next
Bolton Bailey (Jun 03 2022 at 03:55):
Is there a function of type fin n -> fin n which maps i to i+1, wrapping around to 0 for i = n-1, which works for n=0 and n=1?
Eric Rodriguez (Jun 03 2022 at 05:18):
(+ 1)
Kevin Buzzard (Jun 03 2022 at 05:57):
Won't that say "what the heck is 1" if n is small?
Eric Rodriguez (Jun 03 2022 at 06:18):
Oh, d'ah, yes. I checked whether the add is defined but I didn't check for 1
Yakov Pechersky (Jun 03 2022 at 06:32):
Notification Bot (Nov 21 2022 at 07:43):
Bolton Bailey has marked this topic as unresolved.
Bolton Bailey (Nov 21 2022 at 07:44):
What about a function fin n -> {nat, int} -> fin n that applies fin_rotate a number of times given by the second argument?
Eric Wieser (Nov 21 2022 at 07:46):
Eric Wieser (Nov 21 2022 at 07:46):
Or just raise rotate to a power?
Last updated: Dec 20 2023 at 11:08 UTC