Timo Carlin-Burns

Option to only ignore fork activity that happened prior to forking (alternative to --skip-fork)

3

I'm working with a company that uses repoXplorer to show [their development activity](https://holo.host/activity/). For their use-case, they don't want to ignore forks entirely, (i.e. using `repoxplorer-github-organization --skip-fork`), rather, they want...

In-game hypo inconsistent unknown cards.

13

 1. See a drawn card in the present game 2. Enter replay and rewind to the first turn 3. Enter in-game hypo - Any drawn card...

Often when I'm spectating a review, I start by going over the moves by myself to catch up to where the team is. If during this time the review leader...

refactor: clean up public API around `Array.eraseIdx`

1

- Removes the public definitions `Array.eraseIdxAux` and `Array.eraseIdxSzAux` which were implementation details. - Motivation: `Array.eraseIdxAux` and `Array.eraseIdxSzAux` were clearly not intended to remain public, but simply making them private would...

feat: `Small.{u}` sets are closed under various operations

2

This PR adds lemmas showing that sets constructed by applying basic set operations to small sets are themselves small. We now have corresponding `Small ↥s` versions of almost all of...

Make errors on Arch

2

OS: GNU/Linux Distro: Arch Linux Kernel: 4.8.13-1-ARCH [`make` output](https://gist.github.com/timotree3/44eab1da5c223dda1e57bad17e6e2c44) [`make test` output](https://gist.github.com/timotree3/c2c1497fbc0c020d03be1147c4015783)

This is not true if two people publish the exact same happ. In that case there are two HHA hashes which both have the same DNA hash. https://github.com/Holo-Host/holo-envoy/blob/898ad4b49fdd7d1c42d01dbe39328ab4cdf7ce9b/src/index.ts#L1209-L1231

fix: remove special handling of numerals in `DiscrTree`

10

Fixes https://github.com/leanprover/lean4/issues/2867 by removing special handling of `OfNat.ofNat` numerals from `DiscrTree`. The special handling was added in 2b8e55c2f19e6599128bc7e57cb7221df5693b4e to fix a bug represented in the test `tests/lean/run/bugNatLitDiscrTree.lean`, but with https://github.com/leanprover/lean4/issues/2916...