Commit 2025-03-07 09:23 6fcd9b03
View on Github →chore(Control/Random): Use NeZero
instead of returning Fin n.succ
(#22672)
Changes the random generation of Fin
s to take NeZero n
instead of giving a Fin n.succ
.
chore(Control/Random): Use NeZero
instead of returning Fin n.succ
(#22672)
Changes the random generation of Fin
s to take NeZero n
instead of giving a Fin n.succ
.