-
Iavor S. Diatchki authored
The idea is that when we want to match on type level nats, we should use `Nat1`, and use the `FromNat1` function to switch between the structured and unstructured representation of numbers. A bit of custom machinery is needed for this to work properly, because to go back (i.e., to solve FromNat1 x ~ 3) GHC needs to know that FromNat1 is an injective function.
02998bd6