I added new functions and lemmas in Assignment04.v and they work without trouble in CoqIde. As far as I know, most TAs use automatic compiling&grading programs to check students' homeworks. So I wonder: is it okay to add new functions and lemmas? Or does it cause problems in the grading program?
I added new functions and lemmas in Assignment04.v and they work without trouble in CoqIde. As far as I know, most TAs use automatic compiling&grading programs to check students' homeworks. So I wonder: is it okay to add new functions and lemmas? Or does it cause problems in the grading program?