Assignment 07 Status
jeehoonkang opened this issue · 11 comments
Hi all,
-
Assignment 07 is issued.
-
Please read Homework.md to know how to fetch homework and submit your answer.
- You have to run
./fetch-homework.sh
to get assignment 07. - Do your homework by editing
sf/Assignment07_??.v
. - Make sure
make
works without errors. - Commit and push to your GitHub repository.
- Make sure
https://github.com/$YOURID/pl2015
contains the change you made.
- You have to run
-
Stay tuned for README.md and this issue on the assignment.
-
You are NOT allowed to use the
admit
tactic
becauseadmit
simply admits any goal
regardless of whether it is provable or not.But, you can leave
admit
for problems that you cannot prove.
Then you will get zero points for those problems. -
Do NOT add any additional
Require Import/Export
.
Sincerely,
Jeehoon
I think 'You are NOT allowed to use the following tactics.' should be changed.
이제 SearchAbout 해서 나오는 Theorem들은 다 사용해도 되는건가요?
Is there any grader for ass7 or not?
@Parkdaeyoung I will issue the grader before tomorrow's dawn.
@SungMinCho Yes you can.
@jaewooklee93 Yes you can use those tactics. Thank you for pointing out that.
I would like to announce that you ARE allowed to use the following tactics for the assignment 07 and so on:
`tauto`, `intuition`, `firstorder`, `omega`.
Jeehoon
Now you can grade your submission by yourself: http://sf.snu.ac.kr/jeehoon.kang/pl2015/Assignment07_grader.tar.gz
Submissions are collected.
when is deadline for delay of assignment 07?
Today 14:00.
Delay submissions are collected.