search

snu-sf-class / pl2016

14 stars 17 forks source link

Can I use Require Export in assignment? #32

Closed shuuki4 closed 8 years ago

shuuki4 commented 8 years ago

Assignment 2에서 앞서 증명한 Theorem을 사용하려고 하는데, 파일이 별개로 되어있어서 불러올 수가 없습니다. 앞선 파일에서 증명한 것을 들고 오기 위해 Require Export 문을 사용해도 되는건가요?

jeehoonkang commented 8 years ago
shuuki4 commented 8 years ago

@jeehoonkang 그러면 증명한걸 복붙해서 다시 쓰는 것 이외에 불러와서 쓰는 방법은 없는건가요? ㅜ.ㅜ

jeehoonkang commented 8 years ago

네.. ㅠ

k32l commented 8 years ago

I didn't get. So we should write all the proved theorem again if we want to use them in the code?

jeehoonkang commented 8 years ago

@k32l Yes you should. It is a little bit clumsy to copy-and-paste lemmas, but please consider that it is essential for automatic evaluation..