Enable TOC and fix minor warnings #602
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Haha, our pre-commit is really strict with us these days:) |
jonaprieto
changed the title
jonaprieto
changed the title
fredrik-bakke
added a commit
to fredrik-bakke/agda-unimath
that referenced
this pull request
May 20, 2023
- Enhance TOC - Solves some warnings seen here: https://github.com/UniMath/agda-unimath/actions/runs/4991616992/jobs/8939272325#step:12:1304 - Closes UniMath#614 - Removes the background from the agda logo. I tried syncing SVG stroke colours with agda-logo.css (so it responds to the colour theme), but no luck yet. We need more time to figure it out. the following is related and the suggestion included in my experiment. - rust-lang/mdBook#773 --------- Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
fredrik-bakke
added a commit
to fredrik-bakke/agda-unimath
that referenced
this pull request
May 28, 2023
commit 3b74252 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 27 22:51:21 2023 -0400 fix indentation commit 880504d Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 27 21:03:31 2023 -0400 remove punctuation at end of headers commit cb2a09c Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 27 21:03:15 2023 -0400 pre-commit autoremove punctuation at end of header commit f19934c Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 27 20:52:42 2023 -0400 add remarks about missing contents commit 582e75c Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 27 20:34:57 2023 -0400 pre-commit detect empty sections at end of file commit 3d53688 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 27 19:45:19 2023 -0400 remove empty code blocks commit 437056c Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 27 19:45:04 2023 -0400 compatibility markdown-conventions and fix-imports commit 8c7f782 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 27 19:38:57 2023 -0400 pre-commit autoremove empty code blocks commit 6f84849 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 14:28:44 2023 +0200 fix some indentation and then give up for the moment commit ccdad61 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 14:05:31 2023 +0200 add `indentation_conventions.py` commit ba930b4 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 13:33:11 2023 +0200 rename pre-commit scripts commit 2cd2433 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 13:09:02 2023 +0200 Add and enforce section conventions commit db60c6f Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 12:07:41 2023 +0200 rename `remove_extra_blank_lines.py` to `blank_line_conventions.py` commit 0d1f085 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 12:05:11 2023 +0200 Fix top section headers not at start of file commit 986a68d Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 11:52:20 2023 +0200 swap to using `_-ℤ_` commit cea0cf6 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 10:53:52 2023 +0200 define infix operator `_-ℤ_` for difference commit b2cd359 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 10:44:42 2023 +0200 Fix empty subsubsections commit ecd6061 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 10:05:23 2023 +0200 fix empty subsections commit 3823a10 Merge: 23e5534 92c52ba Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sun May 21 06:43:30 2023 +0200 Merge branch 'UniMath:master' into modalities3 commit 23e5534 Author: Jonathan Cubides <jonathan.cubides@uib.no> Date: Fri May 19 01:04:26 2023 +0200 Fix: missing logo (UniMath#625) Minor fix due to a local cache issue commit 0ba07cd Author: Jonathan Cubides <jonathan.cubides@uib.no> Date: Fri May 19 00:09:46 2023 +0200 Enable TOC and fix minor warnings (UniMath#602) - Enhance TOC - Solves some warnings seen here: https://github.com/UniMath/agda-unimath/actions/runs/4991616992/jobs/8939272325#step:12:1304 - Closes UniMath#614 - Removes the background from the agda logo. I tried syncing SVG stroke colours with agda-logo.css (so it responds to the colour theme), but no luck yet. We need more time to figure it out. the following is related and the suggestion included in my experiment. - rust-lang/mdBook#773 --------- Co-authored-by: Fredrik Bakke <fredrbak@gmail.com> commit 9b80ef0 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 13 20:29:54 2023 +0200 Remove unused imports and fix some unaddressed comments (UniMath#621) Sorry, my script wasn't finished when I made the last commit in UniMath#620, and here are the remaining unused imports. This PR also fixes some comments I made earlier that went unaddressed. I'm wondering, are the imports scripts interfering with people's merging process a lot? If so, we don't have to merge those changes now. commit 3b658d0 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 13 19:14:02 2023 +0200 Refactor to use infix binary operators for arithmetic (UniMath#620) - Refactor to use infix binary operators for arithmetic. - Define infix binary operators for arithmetic operations on the Eisenstein integers, Gaussian integers,half integers, and truncation levels. - Swap to using left/right instead of a `'` for different laws for binary arithmetic operators. - Some additional refactoring for Eisenstein integers and Gaussian integers Note that the non-infix variants of the operators are still used some places, matching how `Id` and `pair` are used. commit f77b71e Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 13 14:39:13 2023 +0200 Define binary operator notations for `mul-ℕ`, `mul-ℤ`, and `exp-ℕ`. (UniMath#618) They are `_*ℕ_`, `_*ℤ_`, and `_^ℕ_` respectively. In addition to what the title says, I've also refactored the files - `multiplication-natural-numbers` - `multiplication-integers` - `exponentiation-natural-numbers` - `absolute-value-integers` to use the binary operators where it's natural, to get a sense for how this would look. It should be possible to change most usages easily enough* with a nice enough regex, but I don't want to do this before I get some feedback on whether it is preferable. Also, pairs like `is-injective-mul-succ-ℕ` and `is-injective-mul-succ-ℕ'` should perhaps be renamed to something like `is-injective-left-mul-succ-ℕ` and `is-injective-right-mul-succ-ℕ`. commit ee5a96c Author: Egbert Rijke <e.m.rijke@gmail.com> Date: Fri May 12 00:52:35 2023 +0200 Subframes and quotient locales via nuclei (UniMath#613) commit 750f151 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 20 17:16:03 2023 +0200 small fixes commit e1f3af4 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 20 00:40:58 2023 +0200 add `is-emb-map-prod` commit 973a00f Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 20 00:40:29 2023 +0200 fix expressions in some headers commit e3f8a25 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Tue May 16 14:05:02 2023 +0200 Swap from `md` to `text` code blocks (UniMath#622) - Fix diagrams in `pullback-hom` - Swap from `md` to `text` code blocks - Register Collatz' bijection in the OEIS file commit c7398a7 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 13 20:29:54 2023 +0200 Remove unused imports and fix some unaddressed comments (UniMath#621) Sorry, my script wasn't finished when I made the last commit in UniMath#620, and here are the remaining unused imports. This PR also fixes some comments I made earlier that went unaddressed. I'm wondering, are the imports scripts interfering with people's merging process a lot? If so, we don't have to merge those changes now. commit 001e8d7 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 13 19:14:02 2023 +0200 Refactor to use infix binary operators for arithmetic (UniMath#620) - Refactor to use infix binary operators for arithmetic. - Define infix binary operators for arithmetic operations on the Eisenstein integers, Gaussian integers,half integers, and truncation levels. - Swap to using left/right instead of a `'` for different laws for binary arithmetic operators. - Some additional refactoring for Eisenstein integers and Gaussian integers Note that the non-infix variants of the operators are still used some places, matching how `Id` and `pair` are used. commit fde878d Author: Fredrik Bakke <fredrbak@gmail.com> Date: Sat May 13 14:39:13 2023 +0200 Define binary operator notations for `mul-ℕ`, `mul-ℤ`, and `exp-ℕ`. (UniMath#618) They are `_*ℕ_`, `_*ℤ_`, and `_^ℕ_` respectively. In addition to what the title says, I've also refactored the files - `multiplication-natural-numbers` - `multiplication-integers` - `exponentiation-natural-numbers` - `absolute-value-integers` to use the binary operators where it's natural, to get a sense for how this would look. It should be possible to change most usages easily enough* with a nice enough regex, but I don't want to do this before I get some feedback on whether it is preferable. Also, pairs like `is-injective-mul-succ-ℕ` and `is-injective-mul-succ-ℕ'` should perhaps be renamed to something like `is-injective-left-mul-succ-ℕ` and `is-injective-right-mul-succ-ℕ`. commit 76bf8c7 Author: Egbert Rijke <e.m.rijke@gmail.com> Date: Fri May 12 00:52:35 2023 +0200 Subframes and quotient locales via nuclei (UniMath#613) commit 375210c Author: VictorBlanchi <76261859+VictorBlanchi@users.noreply.github.com> Date: Thu May 11 16:49:27 2023 +0200 Iterated cartesian product is closed by permutation (UniMath#617) I have shown that the 3 definitions of iterated cartesian product of types is closed by permutation. commit 730861a Author: Fredrik Bakke <fredrbak@gmail.com> Date: Thu May 11 15:51:39 2023 +0200 alignment of pullback-hom diagrams commit dab6d30 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Thu May 11 12:33:08 2023 +0200 some nitpicking commit 469dba3 Author: Fredrik Bakke <fredrbak@gmail.com> Date: Wed May 10 21:08:12 2023 +0200 wording `26-descent`
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I tried syncing SVG stroke colours with agda-logo.css (so it responds to the colour theme), but no luck yet. We need more time to figure it out. the following is related and the suggestion included in my experiment.