Update README with progress

2026-07-14 15:13:19 +09:00
parent 85f81c8395
commit 502acf8596
1 changed files with 20 additions and 32 deletions
@@ -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)