[isabelle-dev] Numeral_Type.thy

Makarius makarius at sketis.net
Thu Mar 12 20:50:58 CET 2009

On Thu, 12 Mar 2009, Brian Huffman wrote:

> The typed print translation in Numeral_Type.thy, which prints "card 
> (UNIV :: 'a set)" as "CARD('a)", is broken.
> I think it has something to do with the new properly-qualified name for 
> "UNIV" that was introduced recently.
> Anyway, I'm not exactly sure what is going wrong or how to fix it. Does 
> anyone have an idea?

Here is the (old) source:

syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")

translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"

typed_print_translation {*
  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
    Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
in [(@{const_syntax card}, card_univ_tr')]

Above @{const_name UNIV} should be @{const_syntax UNIV} -- this 
corresponds to the CONST marker in the 'translations' specification.

BTW, these markers are smart enough to handle both old and authentic 
syntax as expected.

The former @{const_name UNIV} happened to coincide with @{const_syntax 
UNIV}, because the constant was both global and non-authentic.


More information about the isabelle-dev mailing list