feat: add seal and unseal commands

[leodemoura]

No description provided.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 092ca8530a6f272b7cb19235750479cdffab11de --onto 806e41151b6eb645e4ed5a40915b94b99f933564. (2024-05-02 18:54:59)

[nomeata]

Do we want/need the seal … in $c:command variant, and maybe also the seal … in variant for terms and tactics?

[leodemoura]

Do we want/need the seal … in $c:command variant, and maybe also the seal … in variant for terms and tactics?

We already have it. See new test:

seal f in
example : f x = x + 1 := rfl

[nomeata]

Ah, neat! I didn't expect that after scrolling through the macro definition. Neat.

[Kha]

@nomeata in is a generic command combinator

[nomeata]

But I assume it won’t work scoped around terms and tactics for free, does it?
(Not urgently needed).

I’m a heavy user of unseal already:
leanprover-community/mathlib4@nightly-testing...lean-pr-testing-4061