search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Can I use 'auto' tactic for HW(assignment) and exams? #57

Closed ik1ne closed 9 years ago

ik1ne commented 9 years ago

Can I use 'auto' and 'tauto' tactics?

jeehoonkang commented 9 years ago

Yes.

ik1ne commented 9 years ago

@jeehoonkang Thank you! One more thing to ask, should I close this issue since it is resolved?

jeehoonkang commented 9 years ago

Don't worry; I will close the issue!

jaewooklee93 commented 9 years ago

It is quite surprising that we can use tauto. Since the power of tauto is too strong, the most of exercises in Logic.v can be solved even in simple one line unfold iff; unfold not; tauto....

gilhur commented 9 years ago

You are not allowed to use 'tauto' yet. More specifically, you are not allowed to use the following tactics.

[tauto], [intuition], [firstorder], [omega]

At some point later, I will allow to use them, but NOT YET!