From 502acf859676bf7f6e384ef8a4174b1717d929dc Mon Sep 17 00:00:00 2001 From: h7x4 Date: Tue, 14 Jul 2026 15:13:19 +0900 Subject: [PATCH] Update README with progress --- README.md | 52 ++++++++++++++++++++-------------------------------- 1 file changed, 20 insertions(+), 32 deletions(-) diff --git a/README.md b/README.md index 59b7ffb..0ecb845 100644 --- a/README.md +++ b/README.md @@ -1,38 +1,26 @@ # Software Foundations 1 -This is a template repository for the code found in [Software Foundations 1](https://softwarefoundations.cis.upenn.edu/lf-current/index.html) +This is my instance of [Software Foundations 1](https://softwarefoundations.cis.upenn.edu/lf-current/index.html) -It contains an additional nix-shell and envrc file to easily get started. +### Progress -All the HTML has been removed, most of the content is inlined in the files anyway, and the rendered HTML is available online if you need it. +- [X] Basics +- [X] Induction +- [X] Lists +- [X] Poly +- [X] Tactics +- [X] Logic +- [ ] IndProp + - [ ] Rel + - [X] ProofObjects + - [ ] IndPrinciples + - [ ] Maps + - [ ] Imp + - [ ] ImpParser + - [ ] Extraction + - [ ] ImpCEvalFun + - [ ] Auto -Fork me, and go ham. +### Suggested Roadmap -![Deps](./deps.svg) - ---- - -## Original README - -``` -######################################################################### - SOFTWARE FOUNDATIONS -######################################################################### - -This directory contains both Rocq scripts (.v files) and generated HTML -files for Volume 1 of the Software Foundations electronic textbook -series. - - - Preface.v or Preface.html - The place to start reading, including details on how to install - required software - - - index.html - The book's cover page and navigation starting point - - - deps.html - Overview of the ordering of chapters - - - LICENSE - Explanation of how these files may be redistributed -``` +![Deps](./deps.svg) \ No newline at end of file