Email Gateway (Aug 18 2022 at 12:45): Email Gateway (Aug 18 2022 at 12:45):From: Jens-Wolfhard Schicke <drahflow@gmx.de>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Hi, I discovered an unfortunate display problem, if not bug:
lemma bug:
assumes assm: "P t"
shows "\<all>t. P t"
proof (rule allI)
fix t
show "P t"
apply (insert assm) (* Proof state: P t ==> P t *)
apply assumption (* Fails, which is A Good Thing *)
In particular the insert should either warn about doubly used variable
names or rename some other variable.
Best Regards,
Jens
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
iEYEARECAAYFAkkzsL0ACgkQzhchXT4RR5BwzgCfZvnfxGdXvwg0i+EouzO3+RDH
foMAnjAUqOASaP28NHfA9cCRKWDZwByN
=kqgw
-----END PGP SIGNATURE-----
Email Gateway (Aug 18 2022 at 12:48):From: Amine Chaieb <ac638@cam.ac.uk>
Hi Jens,
The System somehow warns you in the following sense:
Lokk at the proof state after
apply (insert assm)
Then you will notice that one t is "brown" and the other is blue. These
colors have a meaning and they depend on the nature of the
binding/declaration of the variables, which gives you some insight about
what you are writing.
This feature saved me a lot of time on several occasions!
Hope it helps,
Amine.
Jens-Wolfhard Schicke wrote:
Last updated: May 03 2024 at 08:18 UTC