Stream: Beginner Questions

Topic: Record update syntax

view this post on Zulip Gergely Buday (Apr 18 2023 at 15:03):

Is there a record update syntax for this kind of tuples?

datatype state = Data (numbers: "int list") (clock: nat)

view this post on Zulip Gergely Buday (Apr 20 2023 at 07:56):

The file src/HOL/ex/Datatype_Record_Examples.thy introduces this. One needs a manual setup for this, though, it is written in the file.

Last updated: Apr 28 2024 at 16:17 UTC