Re: [isabelle] read/print consistency?

> I would say that the "show types" and "show sorts" options were designed
> solely for making terms easier for humans to parse; I don't think any
> guarantees about re-parsing by Isabelle were intended.

'Fraid you are right, Brian. Although these options do help ;-)


> On Mon, May 11, 2009 at 6:14 PM, Chris Capel <pdf23ds at> wrote:
>> Is there supposed to be any sort of guarantee of consistency between a
>> term A and the term B that results from printing A and then reading
>> the result, when the "show types" option is off? I have found a case
>> where the types in B are more general, in a way that caused problems
>> trying to do a lemma. I can give more details if desired.
>> Chris Capel
>> --
>> "What is it like to be a bat? What is it like to bat a bee? What is it
>> like to be a bee being batted? What is it like to be a batted bee?"
>> -- The Mind's I (Hofstadter, Dennet)

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