The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

lando wrote:
> 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
>    

Maybe you want [Eval compute] instead of [Eval simpl].  The definition 
of the [simpl] reduction strategy is that it only unfolds definitions 
when that leads to immediate reduction of pattern-matching.  There are 
no [match] expressions in the definition of [andb3], so [simpl] will 
never unfold [andb3].

P.S.: You mention "basics.v" like it is a file that folks on this list 
will be familiar with.  I, at least, don't know what you're referring to.