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     
   [("b",HOLogic.boolT,Syntax.NoSyn)]]*}

(*This is:
record foo =
  b::bool
*)

(* Provided the type, you can get the fields of the record the following 
way:*)
ML {*
val thy = the_context ();
RecordPackage.get_recT_fields thy 
  (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.

   Norbert 






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