Daniel Weber

The default `formatVersion` [here](https://github.com/TheMrZZ/sandstone/blob/master/src/datapack/saveDatapack.ts#L72) and [here](https://github.com/TheMrZZ/sandstone/blob/master/src/datapack/packMcMeta.json#L3) should be 9, not 6.

There isn't a type-safe way to create custom worldgen in Sandstone datapacks.

There isn't a (nice) way to add the new "filter" field to `pack.mcmeta` when creating a datapack with sandstone

Update animator.js

2

Fixed the save_start icon and updated pack_format in the Java Item Model Animator plugin.

feat: define Gray code

2

--- Define binary reflected gray code, both as a permutation of `Nat` and as a permutation of `BitVec n`, and prove some theorems about them. Additionally, remove `@[simp]` from `Nat.bit_false`...

feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size

2

Remove `@[simp]` from `Nat.bit_false` and `Nat.bit_true`, as `bit0` and `bit1` are deprecated, and add some lemmas to `Bits`, `Bitwise` and `Size`. --- [](https://gitpod.io/from-referrer/)

noncomputable section isn't shown anywhere

2

When a definition appears in a `noncomputable section`, while the definition is actually noncomputable, there is no indication given for that anywhere in the docs, and it appears just like...

feat: prove Cauchy's upper bound on polynomial roots

4

--- - [x] depends on: #16582 [](https://gitpod.io/from-referrer/)