The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Andrew McCreight 
<andrew.mccreight AT yale.edu>:


> ...which is a bit more illuminative.

It seems indeed to be a problem of coercion:

The two versions of test check perfectly :

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

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):Set) with
     ta => true
   | tb => 1
   end.


But let us check the if expression alone :

Variable b : bool.
Check (if b then nat else bool).
(*
if b then nat else bool
     : Set
*)


Pierre



>
> -Andrew
>
> On Tue, 12 Apr 2005, 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
> >
>
> --------------------------------------------------------
> 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
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.