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

Formatting fixes #530

Merged
merged 15 commits into from
Mar 21, 2023
Merged

Formatting fixes #530

merged 15 commits into from
Mar 21, 2023

Conversation

fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Mar 21, 2023

Just a bunch of miscellaneous formatting.

  • Fix capitalization of module titles
  • Make comment headers into actual headers
  • Remove some superfluous whitespace
  • Organize VSCode settings
  • Add VSCode settings that nest ".agdai" and ".agda~" files under the associated ".lagda.md" file to declutter the file view.
  • Fix a breaking bug with generate_main_index when there are duplicate titles
  • Add <details> blocks to all files (except foundation-core.universe-levels)
  • Remove unused imports

@fredrik-bakke
Copy link
Collaborator Author

fredrik-bakke commented Mar 21, 2023

I'll spare anyone from having to go through these changes, but I would like to point out one issue that remains.

There is a big bunch of references to theorems and exercises in the library without referencing any book. I am okay with having a section header state

### Theorem 12.3

But then the source should be referenced. Therefore, I've left headers like this as comments for now.

@fredrik-bakke fredrik-bakke marked this pull request as ready for review March 21, 2023 17:15
@fredrik-bakke fredrik-bakke marked this pull request as draft March 21, 2023 17:16
@fredrik-bakke fredrik-bakke marked this pull request as ready for review March 21, 2023 19:26
@fredrik-bakke
Copy link
Collaborator Author

I will merge this PR once the check has finished.

@fredrik-bakke fredrik-bakke merged commit ccbaa46 into UniMath:master Mar 21, 2023
@fredrik-bakke fredrik-bakke deleted the refactor branch March 21, 2023 19:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant