Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
Is there some way to encode type of numbers lower than or equal to some constant n
data Fin n where
FZ :: Fin n
FS :: Fin n -> Fin (S n)
That is, maybe I'm searching for some way to compare const generics at compile time?