직접 해 보기🔗

저장소를 받고 나서:

lake exe cache get        # Mathlib 캐시. 처음 한 번만
lake build
lake exe grade --chapter 1

lake exe grade가 아직 안 채운 연습을 표로 보여 준다. Reynolds/Exercises/Ch01/에서 sorry를 찾아 지우고 채운 뒤 다시 돌리면 된다.

막히면 docs/solving-guide.md를 먼저 봐라. 이 저장소가 반복하는 증명 패턴 넷과 자주 만나는 오류 메시지가 정리되어 있다.