Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
ValidBonuses : Vect n (Fin (S PinCount)) -> Type
ValidBonuses {n = Z} bonuses = LTE 0 0 -- 1) No bonuses, no constraints
ValidBonuses {n = (S _)} bonuses = -- 2) In case of bonuses:
Either -- Either:
(finToNat (head bonuses) = PinCount) -- * The first roll is 10
(sum (map finToNat bonuses) `LTE` PinCount) -- * Or the sum is less than 10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.