Re: [Haskell-cafe] induction on type-level Nat

16 Jan 2023


      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