The Coq mailing list

[Geoff Reedy <geoff AT programmer-monk.net>]

On Tue, Oct 15, 2013 at 12:47:15PM -0700, t x said
> I've written the following example. Assertion 4 seems to imply that the
> type of E need not be fixed.
> 
> (* Assertion 4: the type of lst doesn't have to be fixed
>    Our return type can be function of both the
>      _value_ AND _type_ of the discremee *)
> Definition black_magic (n: nat) (lst: iList n) :=
>   match lst as y in iList n return if (NPeano.odd (n + sum lst)) then Cat 
> else Dog with
>     | _ => match (NPeano.odd (n + sum lst)) as y in bool return if y then 
> Cat else Dog with
>                | true => cat
>                | false => dog
>              end
>   end.

It should go with out saying that lst has only one type, namely iList n.
The "in iList n" just creates a name (n) for the index of iList that can
be used in the return annotation. It is maybe less confusing to give a
different name that doesn't shadow the argument to black_magic:

Definition black_magic (n: nat) (lst: iList n) :=
  match lst as y in iList m return if (NPeano.odd (m + sum lst)) then Cat 
else Dog with
    | _ => match (NPeano.odd (n + sum lst)) as y in bool return if y then Cat 
else Dog with
               | true => cat
               | false => dog
             end
  end.