search

snu-sf / sflib

1 stars 10 forks source link

<< >> 대신 다른 syntax 사용? #5

Open alxest opened 7 years ago

alxest commented 7 years ago
  1. (major) coq mode가 << >> 를 제대로 인식해서 indent 해주지 않음. 
    <<a>> /\
             <<b>>

    이런 식으로 됨.

workaround로 ()로 감싸주면 괜찮아짐.

(<<a>>) /\
(<<b>>)

coq mode indenting rule을 고치는게 가능하면 그게 정해일 듯.

  1. (minor) monad notation과 충돌
alxest commented 7 years ago

a.(b) notation도 coq mode가 엉뚱하게 이해하는데 이것도 매우 불편함. coq mode를 언제 날잡고 고쳐야 할 듯