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 *)
[RecordPackage.add_record_i (,"foo") NONE
record foo =
(* Provided the type, you can get the fields of the record the following
val thy = the_context ();
(Type ("Scratch.foo.foo_ext_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