tpl-in-lean

저장소 구조🔗

Reynolds/Answers/ChNN/

완성본. 이 문서가 인용하는 대상이고, 설명은 전부 이쪽 docstring 에 있다.

Reynolds/Exercises/ChNN/

같은 구조에서 연습 지점만 sorry 로 비운 것. scripts/gen-exercises.py 가 완성본에서 만들어 낸다. 교재 변경은 생성기를 거치고, 개인 풀이 브랜치에서는 sorry 자리에 증명을 직접 쓴다.

ReynoldsTests/

#guard 단위 테스트. 완성본만 import 한다.

docs/

장별 형식화 설계와 연습 푸는 법.

manual/

이 문서.