The Coq mailing list

["Patricia Peratto" <psperatto AT adinet.com.uy>]

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).