Stop learning alone!

Learn faster and stay on-track by joining this free class with other self-learners.

Register for Coq theorem prover now.

Coq theorem prover

Class length: 1 weeks. Start anytime.

Creator: Blasa

Status: Under Construction

 Join this class!
Class Forum » andb3 (better formatting)

andb3 (better formatting)

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?

lando
1 year ago

Reply

Found an answer on the coq-club mailing list. Looks like Eval simpl doesn't reduce definitions if it helps with pattern matching. Instead of Eval simpl using Eval compute solved the problem. I'll have to look further into this in the future.

lando
1 year ago

Reply

* Markdown Cheatsheet:

Link:
[clickable text](http://www.example.com)

New Paragraph:
Hit enter twice

Main heading:
# Main Heading Text

Sub-heading:
## Sub-heading Text

List:
* item 1
* item 2
* item 3

Italics:
*italicized text*

Bold:
**bold text**

YouTube:
URL (http://www.youtube.com/watch?v=Ui4AYPcRkYE) turns into embed code

Full Markdown reference