The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

IMO, the semantics of if in Coq is terrible. You want to use match just about 
anywhere.
Secondly, there are no "untagged unions" in Coq, so you have to take off your 
Lisper hat and put on a crown of thorns if you want to program that way. All 
unions must be explicitly tagged.
In your case you might want to even propagate information learned from the if 
from the returned value. You don't get that for free either. You have to pair 
the result with a proof witness.
-Ian

----- Original Message -----
From: "Patricia Peratto" 
<psperatto AT adinet.com.uy>
To: "coqclub" 
<coq-club AT inria.fr>
Sent: Monday, February 11, 2013 3:23:28 PM GMT -05:00 US/Canada Eastern
Subject: [Coq-Club] if with different types


Is it possible to define an if expression 
that gives values of different types in 
cases true and false? 

For example, I can define the following 
_ifT expression 

Definition _ifT (A:Type)(b:bool)(e1:A)(e2:A):A 
:= bool_rect (fun (b:bool) => A) e1 e2 b. 

and using it I can define as type: 

Definition type1 (b:bool) : Set := 
_ifT Set b nat bool. 

Now I want to define a function that 
gives O in case b is true and gives 
true in case b is false. 

I have done the following definition: 

Definition function1 : forall (b:bool),(type1 b):= 
fun (b:bool) => _ifT (type1 b) b O true. 

But I get the error message 

Error: In environment 
b : bool 
The term "0" has type "nat" while it is expected to have type "type1 b". 

The question is how can I define function1 (using if).