Skip to content

Commit

Permalink
remove NullHomotopy from STYLE.md
Browse files Browse the repository at this point in the history
<!-- ps-id: 8b5dfef3-90a9-42e9-9b23-94addade9985 -->

Signed-off-by: Ali Caglayan <[email protected]>
  • Loading branch information
Alizter committed Dec 19, 2024
1 parent d9f740d commit 47e2e93
Showing 1 changed file with 4 additions and 5 deletions.
9 changes: 4 additions & 5 deletions STYLE.md
Original file line number Diff line number Diff line change
Expand Up @@ -111,11 +111,10 @@ corresponding file `Foo.v` that imports everything in the subdirectory.

- There are files in the root `theories/` directory, including
`EquivGroupoids`, `ExcludedMiddle`, `Factorization`, `HFiber`,
`Extensions`, `NullHomotopy`, `Projective`,
`Idempotents`, `Constant`, `BoundedSearch`, etc. These contain more
advanced results which may depend on files in the whole library. We
try to limit the number of files in the top-level folder, and would
like to reduce the number.
`Extensions`, `Projective`, `Idempotents`, `Constant`,
`BoundedSearch`, etc. These contain more advanced results which may
depend on files in the whole library. We try to limit the number of
files in the top-level folder, and would like to reduce the number.

- `WildCat/*`: Files related to wild categories. They are used
extensively in the library, so we try to minimize the files they
Expand Down

0 comments on commit 47e2e93

Please sign in to comment.