-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
Yes, of course! Stupid me, thanks for pointing that out Daniel.
Now it works as expected.
Florian
On 09/22/2012 12:55 AM, Daniel Peebles wrote:
> Shouldn't you have
>
> IxZero :: Ix (CtxCons ty ctx) ty
>
> instead of
>
> IxZero :: Ix ctx ty
>
>
Shouldn't you have
IxZero :: Ix (CtxCons ty ctx) ty
instead of
IxZero :: Ix ctx ty
On Fri, Sep 21, 2012 at 8:34 AM, Florian Lorenzen <
florian.loren...@tu-berlin.de> wrote:
> -BEGIN PGP SIGNED MESSAGE-
> Hash: SHA1
>
> Hello cafe,
>
> I have the following GADT definitions capturing th
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
Hello cafe,
I have the following GADT definitions capturing the simply typed
lambda calculus with de Bruijn indices for variables and explicitly
annotated types for variables:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataK
