(* Change every field in a record type to have integer type *) con allInts = fold (fn r :: {Type} => {Type}) (fn tname :: NameOpt => fn name :: FieldName => fn t :: Type => fn tail :: {Type} => fn acc :: {Type} => [[name : integer]] ++ acc) (Empty(Type)) (* Build a function for adding the fields of an all-integer record *) val adder = fold con (fn r :: {Type} => $(allInts r) -> integer) (fn tname :: NameOpt => fn name :: FieldName => fn t :: Type => fn tail :: {Type} => fn acc : ($(allInts tail) -> integer) => (fn r : $([[name : integer]] ++ allInts tail) => #name r + acc r)) (fn r : $(Empty(Type)) => 0)