Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change numbering of sHoTT files #36

Open
jonweinb opened this issue Jul 31, 2023 · 5 comments
Open

Change numbering of sHoTT files #36

jonweinb opened this issue Jul 31, 2023 · 5 comments

Comments

@jonweinb
Copy link
Collaborator

I think as a leftover from some older way of organizing the numbering of the files in the sHoTT directory starts at 03. This should really be 01. The file names and all references in the .md files should be changed accordingly.

@emilyriehl
Copy link
Owner

Fine with me.

@emilyriehl
Copy link
Owner

The original file numbering pairs with the sections of the RS paper. But this makes less sense now that we're adding in stuff from your paper. So I agree that we should just simplify and start numbering from 1 (or 0 to be consistent with the HoTT files).

@jonweinb
Copy link
Collaborator Author

Oh of course, I completely forgot about that even being the reason...
I'm fine with either starting at 0 or 1.

@fizruk
Copy link
Collaborator

fizruk commented Jul 31, 2023

I suggest to wait for imports to appear in rzk (see rzk-lang/rzk#71).
Then we won't have to use numbers in the filenames and have more flexible organisation of files overall.

@jonweinb
Copy link
Collaborator Author

Great idea, thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants