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