Polytopes
Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.
Created on 2022-03-12.
Last modified on 2023-05-06.
Files in the polytopes folder
module polytopes where open import polytopes.abstract-polytopes public
Recent changes
- 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).
- 2023-03-12. Fredrik Bakke and Jonathan Prieto-Cubides. Generate module indexes (#501).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).
- 2023-03-03. Jonathan Prieto-Cubides. Hide imports, toc and many other fixes (#480).
- 2023-02-13. Jonathan Prieto-Cubides. Nueva era (#445).