Re: [isabelle] lexical matters

On Mon, 17 Jan 2011, mark at wrote:

Is there a printing mode for type-annotating constants and/or variables with their types (like in HOL4)? I'm concerned about the risk of statements being displayed in a misleading way.

You can implement your own in user space. These things are not part of the kernel. Even the ML toplevel pretty printer can be modified in user space.

Anyway, do you now the funny paper about by Freek Wiedijk, UITP 2010?

I've known this "issue" ever since I got exposed to Isabelle for the very first time, in summer 1993.


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