Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Followup: Unexpected warning about missing map...

view this post on Zulip Email Gateway (Feb 17 2025 at 09:32):

From: Gunnar Teege <cl-isabelle-users@lists.cam.ac.uk>
Followup:

The warning is also signaled if I define the quotient_type for the
record type scheme ('a,'m) record_ext.

Gunnar

smime.p7s

view this post on Zulip Email Gateway (Feb 17 2025 at 09:43):

From: Gunnar Teege <cl-isabelle-users@lists.cam.ac.uk>

Followup:

The warning is also signaled if I define the quotient_type for the
record type scheme ('a,'m) record_ext.

Sorry, of course I meant the record type scheme ('a,'m) myrec_ext.

Gunnar

smime.p7s

Last updated: Mar 09 2025 at 12:28 UTC