Re: [isabelle] Code equations for UNION in Isabelle2012-RC1

Hi Florian,

thanks for the explanation (and solution). So far, abbreviations in export_code statements either worked for me or I got an error about "not a constant". Is there a rule of thumb when the code generator accepts to generate code for type-constrained constants?

For example, of the following abbreviations, x y and z work, although they specialize types, but u does not. What is the fundamental difference?

abbreviation x :: nat where "x == 0" (* overloaded constant *)
abbreviation y :: "nat => nat => nat" where "y == op +" (* overloaded operator *)
abbreviation z :: "nat => nat => nat" where "z == power" (* definition in type class *)
abbreviation u :: "(nat => bool) => nat" where "u == Least"


Am 04.05.2012 16:20, schrieb Florian Haftmann:
theory Scratch imports Main begin
export_code UNION in SML file -

*** Type
*** 'a::type set => ('a::type => 'b::type set) => 'b::type set
*** of constant "Complete_Lattices.complete_lattice_class.SUPR"
*** is too specific compared to declared type
*** ?'b::{} set => (?'b::{} => ?'a::{}) => ?'a::{}
*** At command "export_code"

the issue is simple: UNION is just an abbrev for SUPR at a certain type, and
therefore has a »too specific« type. Want you want is:

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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