Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOLCF and records

view this post on Zulip Email Gateway (Aug 18 2022 at 15:20):

From: Saidai no <saidai-no@saidai-no.name>
Hello

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

Regards,
Maxim

view this post on Zulip Email Gateway (Aug 18 2022 at 15:20):

From: Alexander Krauss <krauss@in.tum.de>
Dear Maxim,

This is a known bug, which has been fixed in the development branch
already. It will work in the next Isabelle release.

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 15:20):

From: Makarius <makarius@sketis.net>
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

Last updated: Nov 21 2024 at 12:39 UTC