읽는 순서
파일마다 docstring 첫머리에 "읽는 순서"가 적혀 있다. 처음 오는 사람을 위해 한자리에 모은다.
-
Background.lean— 메타언어와 객체언어. import 순서와 달리 학습 순서에서는 첫 파일이다 -
Syntax.lean— §1.1 추상 구문 -
Notation.lean— §1.1 구체 구문. 객체 언어를 Lean 표기로 쓰는 DSL -
Semantics.lean— §1.2 표시적 의미론 -
Validity.lean— §1.3 타당성, 추론 규칙, 건전성 -
FreeVars.lean— §1.4 자유 변수와 일치 정리 -
Substitution.lean— §1.4 치환, 명제 1.2 ~ 1.5 -
Realizations.lean·Realizations/,Ex.lean,Ex/Summation.lean— 책 연습문제 -
Design.lean— 정의 선택과 정리의 성립. 틀린 정의가 무엇을 깨뜨리는지 -
Depth/— 심화 트랙. 건너뛰어도 1장은 완결된다
전부 Reynolds/Answers/Ch01/ 아래에 있고, 같은 구조가 Reynolds/Exercises/Ch01/에도
있다. 그쪽은 연습 지점만 sorry로 비어 있다.
연습은 Ex.lean에만 있지 않다
이름 때문에 오해하기 쉬운 자리가 있다.
책의 명제 1.1 ~ 1.5 증명이 본문 파일 안에 연습으로 들어 있다. FreeVars.lean의 일치 정리, Substitution.lean의 치환 정리,
Validity.lean의 건전성이 그렇다.
Ex.lean의 연습 1.4는 앞에서 정의한 포획 회피 치환을 실제 구문에 적용한다. 따라서 본문 파일을 건너뛰면
문제의 전제가 되는 정의와 보조정리를 아직 보지 않은 상태가 된다. 처음 읽을 때는 위 목록의
1 ~ 7을 따라가고, 이후에는 필요한 정리의 선언 위치로 돌아오면 된다.
무엇이 어디에 몇 개 있는지는 아래 연습문제 절에 있다.