Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Fri, 16 Apr 93 12:22:22 EDT
From: shb@com.oracorp
Message-Id: <9304161622.AA13765@sparta.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Records in HOL object language?

What HOL object-language constructs would people recommend that I use
when what I'd really like are record-valued (in C, structure-valued)
functions?

I'll have "before" states that are essentially tuples of functions
which map objects to records containing a dozen or so pieces of
information about each object, pieces of information of two to a few
different types.  I'll want to compute and reason about "after" states
that typically differ from the "before" states only in one function,
where that function's value is only changed for one or two objects, and
where the function's value on these objects is only changed for one to
a few of the pieces of information.  The problem is defining things in
a consistently-typed way for related but differently-typed pieces of
information, conveniently accessing this information, and conveniently
describing small changes to this information.  I've got a few ideas,
but would like to hear what others say before I start implementing.

I have vague possible memories of a discussion of this before, but
can't find it in the info-hol archive's index.  

Steve Brackin
ORA