The Coq mailing list

[lando <lando2 AT gmail.com>]

Thanks for the quick reply.  I'll check it out.  Working from a basic
introduction and haven't gotten to compute yet.

As far as the references to Basics.v go, I thought they were standard
issue url's are as follows.
http://www.seas.upenn.edu/~cis500/cis500-s09/lectures/Basics.pdf
http://www.seas.upenn.edu/~cis500/cis500-s09/hws/Basics.v

On Sat, Apr 17, 2010 at 8:15 PM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> 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.
>