theory week09A_demo_records
imports Main
begin

record A = a :: nat
           b :: int

term "\<lparr>a = 3,b = 4\<rparr>"
term a
term b
term a_update

(* notice that the name is global; try to give longer names,
     otherwise 'a' is taken for the rest of the theory *)

consts r :: A
term r
term "a r"
consts re :: "unit A_scheme"
consts rf :: "int A_scheme"

term re
term rf

term "A.more"
term "A.more re"

record B = A + c :: "nat list"

consts rb :: B
term rb
term "B.more rb"
term "A.a rb"
term B.more
term A.more

consts f :: "'a A_scheme \<Rightarrow> unit"
consts g :: "A \<Rightarrow> unit"

term "f rb" \<comment> \<open>extended record types are subtypes of the record schemes they extend \<close>
term "f r"
term "g rb" \<comment> \<open>..but not of the unparameterised record type \<close>

end
