연습문제🔗

1장에는 채점되는 연습이 37개 있다. 책 연습문제와 본문 명제가 섞여 있고, 아래는 읽는 순서와 같은 차례로 늘어놓은 것이다.

• Validity.lean — §1.3 건전성과 규칙. 3개

• FreeVars.lean, Substitution.lean — 본문 명제 1.1 ~ 1.3. 5개

• Realizations/Constructors.lean, Ex.lean — 책 연습 1.1 ~ 1.4. 12개

• Ex/Summation.lean·Ex/Summation/ — 책 연습 1.5 · 1.6. 7개

• Design.lean — 정의 선택과 정리의 성립. 3개

• Depth/ — 심화 트랙. 7개

본문 명제를 건너뛰면 책 연습에서 쓸 재료가 없다.

명제 1.1(정수 식 판, coincidence_intExp)과 명제 1.5는 파일에 있지만 채점 대상이 아니다. 방향이 서로 반대다 — 정수 식 판은 명제 1.1(단언 판)과 명제 1.3 (치환 정리)이 그 결과를 직접 쓰므로 완성된 채로 주고, 명제 1.5는 거꾸로 치환 정리 자체를 쓴다. 채점기는 "이 증명이 sorry에 기대는가"만 보고 그것이 자기 sorry 인지 앞 연습에서 물려받은 것인지 구별하지 못한다. 그래서 비우는 연습들은 서로 의존하지 않도록 골라 두었다.

심화 트랙은 책을 따라가는 데 필요하지 않다. 건너뛰어도 1장은 완결된다.