feat: add `seal` and `unseal` commands

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

Closed leodemoura closed 2 weeks ago

leanprover-community-mathlib4-bot commented 2 weeks ago

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 commented 2 weeks ago

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

leodemoura commented 2 weeks ago

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 commented 2 weeks ago

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

Kha commented 2 weeks ago

@nomeata in is a generic command combinator

nomeata commented 2 weeks ago

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