search

snu-sf-class / pl2016

14 stars 17 forks source link

Assignment 13 #82

Open jeehoonkang opened 8 years ago

jeehoonkang commented 8 years ago

Assignment 13 is issued: https://github.com/snu-sf-class/pl2016#assignments

alxest commented 8 years ago

Ltac을 쓰고 싶은데 이미 정의된 notation과 충돌이 납니다. 이를테면 아래와 같이 정의한다고 하면

match goal with
         | [ H : (_ /\ _) |- _ ] => destruct H end.

이런 에러가 납니다.

Syntax error: '\in' expected after [constr:operconstr level 200] (in [constr:operconstr]).

아래 notation들에서 |- 를 써서 그런 것 같은데,

Notation            Scope     
"'|-' t '\in' T" := Types.has_type t T
                               (default interpretation)
"Gamma '|-' t '\in' T" := has_type Gamma t T
                               (default interpretation)

어떻게 하면 좋을까요?

alxest commented 8 years ago

시험 볼 때도 같은 문제가 있을텐데 해결법이 있으면 좋겠습니다.

alxest commented 8 years ago 
Reserved Notation "Gamma '|-' t '\in' T" (at level 40).

실제로 D.v에서 이 라인 전에는 ltac 정의가 잘 되고 이후에는 안됩니다.

구글링해보니 나오는 글: http://stackoverflow.com/questions/29688939/software-foundations-notation-shadows-ltac-match-notation

jeehoonkang commented 8 years ago

교수님께서 @alxest 님께 답변하셨다고 들었는데, 혹시 답변 내용을 공유해주실 수 있으십니까?

alxest commented 8 years ago

@jeehoonkang |-를 |=로 바꾸자고 하셨습니다.

jeehoonkang commented 8 years ago

어.. 숙제를 바꾸는 건가요?

alxest commented 8 years ago

@jeehoonkang 저도 자세히는 모르겠습니다. 제 생각에는 지금 숙제를 바꾸기는 어려울 것 같습니다. 이와 관련한 컴플레인이 저 혼자였는데, 저는 이번 숙제는 ltac 없이 그냥 했기 때문에, 바꾸지 않으셔도 될 듯 합니다. 다만 시험에서는 충돌이 없었으면 좋겠습니다.

mkh48v commented 8 years ago

이거 써도 되나요? https://github.com/snu-sf-class/pl2015spring/issues/154 여기 누가 증명한 theorem이요

alxest commented 8 years ago

@mkh48v honor code 읽어보세요.

jeehoonkang commented 8 years ago

Delay 기한이 변경되었습니다. 원활한 성적처리를 위해 불가피하게 조치하였습니다. 늦게 공지해드려 죄송합니다.