[Agda] non-constructor indices

[Patrik Jansson]

The panic is clearly a bug, and James proposed a work-around until that 
has been fixed, but in general I think the version with the identity 
proof "inside" the datatype is often the one to choose. Here is a variant:

  data Indexed : Nat -> Set where
    B : Indexed Z
    I : {n m k : Nat} {i : Id (plus n m) k} ->
        Indexed n -> Indexed m -> Indexed k

As to your problem with the termination checker, it cannot see 
termination because the recursive call is "hidden by" / wrapped by 
subst.  It would be interesting to investigate if the checker could be 
told to "inline" definitions like that of subst.

/Patrik



James Chapman wrote:
> Hi,
>
> I don't think it should panic. It looks like you have found a bug in 
> the (brand new) coverage checker.
>
> You should raise it here:
>
> http://code.google.com/p/agda/issues/list
>
> In the meantime you can turn off the coverage checker by putting this 
> at the top of you file:
>
> {-# OPTIONS --no-coverage-check #-}
>
> You can also turn it off on the command line if you want if you're 
> using agda in batch mode.
>
> $agda --no-coverage-check Bug.agda
>
> You first version is accepted then.
>
> This isn't an authoritative answer (I'm not an agda developer) but I 
> hope it helps anyway.
>
> Cheers,
>
> James
>
>
> This message has been checked for viruses but the contents of an 
> attachment
> may still contain software viruses, which could damage your computer 
> system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda