Gergely Buday (Apr 13 2023 at 15:16): Gergely Buday (Apr 13 2023 at 15:16):https://isabelle.in.tum.de/library/Doc/Tutorial/Records.html
gives an example of a record definition
record point =
Xcoord :: int
Ycoord :: int
but Isar Reference talks about the
(| fieldA :: typeA, fieldB :: typeB ... |)
syntax. Which is the currently used syntax for record types? And, which type definition keyword should I use to create such a record type?
Christian Pardillo Laursen (Apr 14 2023 at 06:31):Generally you don't see the (| fieldA :: typeA, ... |) syntax since Isabelle automatically creates a type abbreviation when you define a record, and it doesn't seem super useful to prove theorems about arbitrary record types. You should be fine just using the record keyword to define your records and the resulting type abbreviation to refer to them.
Last updated: Dec 21 2024 at 16:20 UTC