Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] print_record command and extensible record type

Email Gateway (Feb 27 2023 at 11:31):

From: Nicolas Méric <nicolas.meric@lri.fr>
Dear all,
I wanted to print some basic records using print_record and I was unable to
find the type of some of them to pass it to print_record. A really simple
example:

record 'a a =
af :: "'a list"

print_record "'a a"

record ('a, 'b) b = "'a a" +
bf :: "'b list"

print_record "('a, 'b) b"

The second print_record command fails and I get the following error:
Unknown record: ('a, 'b) b

Is there a simple way to specify the type of the record b for print_record?

Best regards,

Nicolas Méric

Last updated: Apr 19 2024 at 20:15 UTC