Assignment 07 Status - Githubissues

jeehoonkang commented 9 years ago

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.
Stay tuned for README.md and this issue on the assignment.
You are NOT allowed to use the admit tactic because admit 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

jaewooklee93 commented 9 years ago

I think 'You are NOT allowed to use the following tactics.' should be changed.

SungMinCho commented 9 years ago

이제 SearchAbout 해서 나오는 Theorem들은 다 사용해도 되는건가요?

Parkdaeyoung commented 9 years ago

Is there any grader for ass7 or not?

jeehoonkang commented 9 years ago

@Parkdaeyoung I will issue the grader before tomorrow's dawn.

jeehoonkang commented 9 years ago

@SungMinCho Yes you can.

jeehoonkang commented 9 years ago

@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

jeehoonkang commented 9 years ago

jeehoonkang commented 9 years ago

Submissions are collected.

quan6791 commented 9 years ago

when is deadline for delay of assignment 07?

jeehoonkang commented 9 years ago

Today 14:00.

jeehoonkang commented 9 years ago

Delay submissions are collected.

snu-sf-class / pl2015spring