Re: [isabelle] Unwanted type annotations



Hi Steffen,

Am 21.05.2013 um 17:42 schrieb Steffen Juilf Smolka <steffen.smolka at in.tum.de>:

> Is there a way to turn this feature off or to predict reliably when annotations are inserted?
> From the code it seems that numerals with polymorphic types are annotated, then again i know @{term 1} is polymorhpic but printed without annotation. I guess I don't understand the code completely…
> 
> The code I am working on equips terms with a minimal set of type annotations which ensures the types of the terms are preserved (when printing and reparsing the terms).

I think I found a workaround. There seems to be no requirement that the term that's printed is type-correct. Hence, you could type all numerals with the type "nat" or "real" or probably even "unit" to avoid the spurious type annotations. For example:

    ML {*
    @{term "0::nat"}
    |> Type.constraint @{typ "'b"}
    |> Syntax.string_of_term @{context}
    |> warning
    *}

Cheers,

Jasmin





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