실습하는 법🔗

소스 파일을 읽을 때는 두 가지 순서 규칙이 있다.

Ch01/Background.lean이 첫 읽기다. 연습은 없지만, 책이 가정하고 넘어가는 메타 수준과 객체 수준의 구분을 여기서 다룬다.

연습은 이름이 Ex 인 파일에만 있지 않다. 책의 명제 증명이 본문 파일 안에 연습으로 들어 있고, 책 연습문제가 그 명제들을 사용한다. 처음에는 장마다 읽는 순서를 따라가야 필요한 정리들이 차례로 나타난다.

그다음은 이렇게 돈다.

1. lake exe cache get 으로 Mathlib 캐시를 받고 lake build (처음 한 번만)

2. Reynolds/Exercises/ 에서 sorry 를 찾아 지우고 채운다

3. lake exe grade 로 확인한다

4. 막히거나 다 풀었으면 Reynolds/Answers/ 의 같은 선언과 비교한다

풀이 브랜치에서 python3 scripts/gen-exercises.py 를 실행하면 채운 증명이 다시 sorry 로 바뀐다. 풀이 PR은 생성 파일 일치 검사를 건너뛰며, Exercises 밖의 파일을 바꾸면 CI가 실패한다.