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:

theory Tst
imports HOLCF
begin

record rec1 =
f1 :: nat

typ rec1

*** 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"

  typ rec1
  "(| f1 :: nat |)"


	Makarius





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