Lines Matching defs:record
9 We define properties of a generic record accessor function and updater
11 address/key, v is a value, r is a record, and (g a r) returns the
12 value set to address a in record r, and (s a v r) returns a new record
13 with address a set to value v in record r.
15 We normalize the record structures (which allows the 'equal-ity based
202 (defthm rcd->acl2-of-record-non-nil
209 ;;;; final properties of record g(et) and s(et) ;;;;
264 :in-theory (disable rcd->acl2-of-record-non-nil)
265 :use (:instance rcd->acl2-of-record-non-nil
279 ;; manipulate record terms which are encountered