finegeometer

Missing information in `elm init` text

1

**Quick Summary:** When I start a project, I want to know if `elm init` will create my project in that folder, or a subfolder. That information is not readily available....

How do I enforce an invariant on a struct?

9

Suppose I have this code: ``` #[derive(Copy, Clone)] struct Vector(i32, i32); impl Vector { fn neg(self) -> Self { Self(-self.0, -self.1) } } ``` I would like to specify that...

Suggestion: provide proof that set-coequalizers of finite sets are finite?

2

I recently found myself in need of a theorem that any set-coequalizer of finite sets is finite. Would it make sense to add this theorem to the standard library, either...

What is the final field in each entry of `transdefs`?

2

In `transdefs.js`, each row has six fields. To the best of my understanding (I'm not an expert), this is what they do. - The transistor id. - The id of...

Potential minor error in paper-qcoh.tex: "ring ℚ of integers".

1

Hi! `paper-qcoh.tex`, on lines 1318 and 1319, contains the phrase "`and~$A$ is the ring~$\QQ$ of integers`". While I admit I'm not fully understanding everything, this seems likely to be an...

60Hz Das on Firefox

3

Recently, the Tetris pieces have been moving significantly faster than normal. After a bit of testing, it seems that the pieces are moving at roughly 60Hz, or twice the maximum...

Hi! I think it would be interesting to try a variation of bingo based on the game [Hex](https://en.wikipedia.org/wiki/Hex_(board_game)). You can see the rules of Hex at the linked Wikipedia page,...

Ordinals

5

I got nerd-sniped into implementing ordinals. I hope this is useful! This is my first time contributing to a project, so please tell me if I'm doing anything wrong. There...

Presheaf categories are locally cartesian closed.

2

Hi! I just spent a while proving that presheaf categories are locally cartesian closed. I feel this ought be in the library somewhere, so I'm sharing the code. Feel free...

## Description of proposed feature The reference describes bookmarks as "one of the most important features of Manim Voiceover". Trying to use them seems to require that I install OpenAI...