Using 'hd' function in nostutter

[HyeongMee]

Hi

I used 'hd' function for the nostutter problem, and succeded in proving all the examples presented. But to do that I copied and pasted the hd function in coqIde. I thought that Lists.v is already required in our homework but it seems like it is not because if I compile the homework without hd function pasted, an error msg that hd has no reference keeps appearing. What should I do? Can I just define hd function in the homework file? - I mean, outside of the given problems, as a separate function. But I am worried becuase the professor said that TA would just copy the given problems only and not the other functions or lemmas outside of the given ones - I guess I heard so;; or Is there any problem in how I compiled the file or edited the file?

Thanks :-D

[jeehoonkang]

• For grading, check your submission with the grader I made: https://github.com/snu-sf/pl2015/issues/69
• It is strange your file does not recognize the hd function. Would you please make a small example code and post it?

Jeehoon

[fortunist]

In Lists.v, hd and tl functions are surrounded with Module NatList. and End NatList.. Further, they use the type natlist which was defined new in module NatList. So you cannot apply that functions in the problem using type list nat, even though you can use them by NatList.hd and NatList.tl.

Addition : I wonder how you could use them just by copying and pasting the definition, despite of the argument types.

[gilhur]

You can just define the hd function in the homework file if you want to use it.