chore: remove unused variables warning showing up in build

[ejgallego]

Opted to fix the warnings instead of silencing them, except for the
case involving a mutual inductive.

I'm surprised by the behavior of the linter there, disabled warning
for now.

[david-christiansen]

One of the things I do when I work with these subsystems is check to make sure that those warnings show up!

It'd be nice to have a solution for including messages that only puts them in the HTML and the IDE, not the command-line build output, but I don't think we're quite there yet (it'll be some combination of storing them in something like a custom info node or environment extension to forward on to HTML, plus converting them to silent messages - we have 70% of this in various places but a systematic approach would be better).

[ejgallego]

I see, I assumed these 4 warnings were not intentional. Let's find a systematic solution.

If these warnings are intended as tests, maybe we should make some tests for them?

How would displaying the warnings only in the IDE / HTML would help here?

[david-christiansen]

The idea is that these modules are intended as content - it's code to be shown in blog posts and the like. When these blog posts talk about code with warnings, it's important that the warning is rendered in the HTML. And while working on the post, it's going to be painful if the warnings aren't visible in the IDE.

I think a proper solution looks something like this:

1. We establish a convention for "content" messages and implement it in SubVerso and Verso. I think there's basically two technical options: a persistent environment extension or a custom infotree node. The former can index based on source positions, the latter gets them for free.
2. We create a version of #guard_msgs that both checks the messages and saves them. This belongs in SubVerso, potentially version-gated to limit development labor. It can be used from Verso as well. This also translates the saved messages into invisible messages so they show up in the IDE appropriately.
3. Verso elaborators for Lean code blocks and the like should consult both the real message log and the saved messages when creating highlighted code/HTML, so they produce the correct output.

Today, we have a few 50% solutions to various parts of this and it would be good to consolidate on a proper fix.

[github-actions]

Preview for this PR is ready! 🎉