Re: [isabelle] normalization method introduces schematic type variables in HOL/Word types



Hi Andreas,

> Why does normalization introduce these type variables at all? Is this
> intended? How can I disable this feature or is this inherent to NBE?

nbe itself does not even permit schematic type variables in results.
The problem stems from the postprocessor.  I guess it is a problem with
hidden polymorphism which escaped attention so far, but it will need
further time to investigate this.

An even more minimal example:

> theory Foo
> imports "~~/src/HOL/Word/Word"
> begin
> 
> definition
>   "example = (1 + 1 :: 4 word)"
> 
> ML {* Code_Simp.dynamic_value @{theory} @{term example} *}
> ML {* Nbe.dynamic_value @{theory} @{term example} *}

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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