Re: [isabelle] HOLCF and records
On Thu, 20 May 2010, Saidai no wrote:
Is it possible to define records in HOLCF (Isabelle 2009-1)?
This code raises an exception:
record rec1 =
f1 :: nat
*** exception TYPE raised (line 311 of "type.ML"): Type variable "?'z" has two distinct sorts
*** At command "typ".
The record definition is not a problem here, but the record pretty printer
has some unpleasant features. You can disable some of them as follows:
ML "Record.print_record_type_abbr := false"
"(| f1 :: nat |)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and