수학자들이 편하게 쓸 수 있는 증명 보조용 프로그래밍 언어 "나비" 만들기.

아직 문법은 못 정했지만 나비가 1차 논리를 다루는 언어였으면 좋겠는데,

일단 정수론부터 나비로 코딩하려다가 막혀가지고,

2차 논리로 넘어가야 되는지 궁금해져서 저 질문을 하게 된 것.

그러나 어설프게라도 할 줄 아는 건 렉서 생성이랑 LALR1 파서 생성 밖에 없다.