search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Question about Assignment 2 #33

Closed jaewooklee93 closed 9 years ago

jaewooklee93 commented 9 years ago

I think some comments given in the Assignment 2 are somewhat misleading. For example, 

(** **** Problem #7 : 4 stars (mult_comm) *)
(** Use [assert] to help prove this theorem if necessary.  
    You shouldn't need to use induction. *)

Theorem plus_swap : forall n m p : nat, 

(** **** Problem #8 : 3 stars (mult_comm) *)

Those comments refer to mult_comm, even though there is no theorem named mult_comm in the whole assignment.

jeehoonkang commented 9 years ago

e59aee9eb6771b953b01534faea885dccc445681

jaewooklee93 commented 9 years ago

Thank you.

But still I am unable to find mult_comm even though

(** **** Problem #8 : 3 stars (mult_comm) *)

remains yet.

Is mult_comm intentionally excluded?

jeehoonkang commented 9 years ago

Hi! I think labels there are not important, and mult_comm is included by mistake. Please solve the question as stated in code (not comment)!

Jeehoon