search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Purpose of "Check" blocks in HW8 #100

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

What are we supposed to do with the check blocks in HW8? For example, in A8_01:

(-- Check --) Check ceval_example2 : (X ::= ANum 0;; Y ::= ANum 1;; Z ::= ANum 2) / empty_state || (update (update (update empty_state X 0) Y 1) Z 2).

This block seems to do the same thing whether I've completed the proof above or not. What is its purpose, and do I need to do anything with it?

jaewooklee93 commented 9 years ago

If you accidentally delete the Qed at the bottom of proof, you cannot execute that Check in CoqIde. I guess that Check is for avoiding such mistakes, or it may be useful for TA's grading purpose.

jeehoonkang commented 9 years ago

Both of @jaewooklee93 's guess are right :-) You just FILL_IN_HERE, and then see if the Check's are good.