Coq theorem prover

Having a couple of problems in andb3 from lesson 1.

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 answer key: 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. Can anyone give me a hint?

You must log in to comment.