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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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