The Coq mailing list

[lando <lando2 AT gmail.com>]

I'm just getting started with Coq and am having a couple of problems
in andb3 from basics.v.

Basic Functions:
Inductive bool : Set :=
  | true : bool
  | false : bool.
Definition ifb (b1 b2 b3:bool) : bool :=
  match b1 with
    | true => b2
    | false => b3
  end.
Definition andb (b1 b2:bool) : bool := ifb b1 b2 false.

My function:
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool := andb (andb b1 b2) b3.

My Eval:
Eval simpl in (andb3 true true true).
Eval simpl in (andb3 false true true).

My Output:
= andb3 true true true
: bool
= andb3 false true true
: bool

Not sure why it is coming out like this. It should be
= true
: bool
= false
: bool

It works with the following:
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
match b1 with
|true => andb b2 b3
|false => false
end.

Which is great I guess, but it should work with my code as well. Not
sure what I am doing wrong here. Any help would be appreciated?