theory week09B_demo_records imports Main begin record A = a :: nat b :: int (* Note that the name is global; try to give longer names, otherwise 'a' is taken for the rest of the theory *) (* record constructor syntax: *) term "\a = 3, b = 4\" (* field names are selector functions *) term a term b (* generic update function for field a: *) term a_update (* syntax for record update; update field a in record x: *) term "x \ a := 3 \" (* note type "'a A_scheme" in the output; it means A and any sub-record of A (more later) *) typ "'a A_scheme" consts r :: A term r term "a r" (* A is really "unit A_scheme": *) consts re :: "unit A_scheme" consts rf :: "int A_scheme" term re term rf (* the implicit field "more" accesses any future extensions of the record *) term "A.more" term "A.more rf" (* record extension syntax: *) record B = A + c :: "nat list" consts rb :: B (* rb is a B record: *) term rb (* B's extension is unit *) term "B.more rb" (* rb has all fields of A *) term "A.a rb" term B.more term A.more (* applies to all sub-records of A *) consts f :: "'a A_scheme \ unit" (* applies to only A *) consts g :: "A \ unit" term "f rb" \ \extended record types are subtypes of the record schemes they extend \ term "f r" term "g rb" \ \..but not of the unparameterised record type \ end