Re: [isabelle] Define records in ML?

On Monday 13 November 2006 16:38, Thomas Bleher wrote:
> > Could someone give me some hints how to
> > * create an Isabelle record in ML?
> > * look up a field in a record by name and determine its type?

(* add_record_i (type-params,record-name) parent-name field-decls thy *)
setup {* 
[RecordPackage.add_record_i ([],"foo") NONE     

(*This is:
record foo =

(* Provided the type, you can get the fields of the record the following 
ML {*
val thy = the_context ();
RecordPackage.get_recT_fields thy 
  (Type ("",[TFree ("'a",Sign.defaultS thy)]))

As far as I can remember the signature of "add_record_i" did not change with 
the reimplementation of records. 

  Hope this helps.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.