Re: [isabelle] Unwanted type annotations



That does the trick!

Thanks,
Steffen

On 21.05.2013, at 19:08, Jasmin Blanchette <jasmin.blanchette at gmail.com> wrote:

> 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.