The Coq mailing list

[Virgile Prevosto <virgile.prevosto AT m4x.org>]

Hello,

Le 04/12/2005, à 02:40:02 PM, Dan Synek a écrit:
> Below is a simple definition of a function "test" which works. However
> 
> if the comment around
> the type specification is uncommented then coq outputs the error
> below.  Since this is the type that coq outputs anyway when asked
> using Check,  it is quiet confusing:

> Inductive Test:bool-> Set := ta:Test true | tb : Test false.
> 
> Definition test (c:bool)(t:Test c)  (* : if c then bool else nat*) :=
>    match t in Test b1 return (if b1 then bool else nat) with
>      ta => true
>    | tb => 1
>    end.

You can obtain a term accepted by Coq (version 8.0pl1) by naming your
return type:
-------------
Inductive Test:bool-> Set := ta:Test true | tb : Test false.

Definition foo:= fun (c:bool) => (if c then bool else nat).

Definition test : forall (c:bool) (t: Test c), foo c :=
fun c => fun t => 
  match t in Test c return foo c with
     ta => true
   | tb => 1
   end.
-------------
[Of course, test has now the type forall c : bool, Test c -> foo c]

I don't know why the expanded version triggers an error, but given that
this one is OK, it might well be a bug.
HTH, 
-- 
E tutto per oggi, a la prossima volta
Virgile