Daniel Weber

I'm fairly sure you actually can't have newlines in NBT text. Are you sure there is any valid output?

> I'm curious what you're using this for - I had it in the back of my mind to remove everything about `bit` at some point I'm using it for...

Perhaps they could all go to `Mathlib.Data.Nat.Bits`? I think I'll try to update #12750 and see what I need

Apologies for the late review, I forgot to send it earlier

From what I can see `noncomputable section` affects [Lean.Elab.Command.Scope.isNoncomputable](https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Command.html#Lean.Elab.Command.Scope.isNoncomputable), but it does need to attempt compilation for everything before it can decide if it should be made noncomputable, so I'm...

bors merge