Stream: Coq devs & plugin devs

Topic: Section trickery

Lasse Blaauwbroek (Apr 07 2022 at 06:12):

What do people think about this snippet:

Section S.
Variables x y : nat.
Definition sx := 1 + x.
Lemma t : sx = 1+y.
Fail clear x.
rename x into x'.
pose y as x.
unfold sx.
unfold x.
reflexivity.
Fail Qed.

Would this be considered a bug? It is a bit inconsistent that clear errors, but rename does not.

Lasse Blaauwbroek (Apr 07 2022 at 06:33):

It looks to me like rename does not type check its result, while clear does perform the type check.

Ali Caglayan (Apr 07 2022 at 08:52):

I believe related to https://github.com/coq/coq/issues/6773

Lasse Blaauwbroek (Apr 07 2022 at 09:18):

Yes, this seems highly related indeed. Thanks for the reference

Last updated: Sep 09 2024 at 06:02 UTC