The Coq mailing list

[Maxime Dénès <Maxime.Denes AT inria.fr>]

Hello,

Your definition of _ifT enforces that e1 and e2 have the same type.

However, you could define function1 as follows:

Definition function1 (b : bool) :=
  if b return (if b then nat else bool) then O else true.

The "return" clause specifies the type you want to return, which will 
itself depend on the value of b.

Hope it helps,

Maxime.

On 11/02/2013 21:23, Patricia Peratto wrote:
> 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).