[Haskell-cafe] induction on type-level Nat

[Henning Thielemann]

On Mon, 16 Jan 2023, Henning Thielemann wrote:

> Alternative approach with a GADT:
>
> data T n a where
>   End :: T 0 a
>   Cons :: a -> T n a -> T (n+1) a
>
> ...
>
> If I add the constraint (1<=n+1) to Cons then the testEnd warning 
> disappears.


This definition looks less stupid and works, too:

data T n a where
    End :: T 0 a
    Cons :: (1<=n) => a -> T (n-1) a -> T n a