The Coq mailing list

[Dan Synek <synek AT cs.ru.nl>]

I was told by Iris Loeb here locally that if I read the manual I would 
fint out that I need to add
a return statement to the if statement.

Definition test (c:bool)(t:Test c) : if c return Type then bool else nat :=
  match t in Test b1 return (if b1 then bool else nat) with
    ta => true
  | tb => 1
  end.
She also told me I would get a better type from the check statement if I 
first did:
Unset Printing Synth.

Dan Synek wrote:

> 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:
>
> The term
> "match t in (Test b1) return (if b1 then bool else nat) with
>  | ta => true
>  | tb => 1
>  end" has type "if c then bool else nat" while it is expected to have 
> type
> "if c then bool else nat"
>
> -----
>
>
> 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.
>
> Check test.
>
> (* Outputs test
>     : forall c : bool, Test c -> if c then bool else nat *)
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
> .