Re: [isabelle] pairs and friends



Dear Jasmin,

On 10/24/2016 11:08 AM, Jasmin Blanchette wrote:
> Dear Thomas,
> 
>> In Isabelle/HOL development version 6703434c96d6 I have the following
>> problem: I want to have a friendly function 'foo' (which I reduced so
>> much, that it does not do anything useful anymore for sake of a minimal
>> example). If I use the type "a list â 'a stream â 'a stream" everything
>> works out as expected, but if I switch to streams of pairs, like shown
>> below I get the following error message:
>>
>> Cannot have type variable "'a" in the argument types when it does not
>> occur in the result type
> 
> Thank you for the bug report.
> 
> In principle, I believe your example could be made to work. Unfortunately, I tried a few solutions and they all break some subtle invariants in our construction. I suspect I would need at least one day to work this out.
> 
> For the moment, I have merely improved the message and documented the limitation.
> 
> How important is this for you? Have you found a satisfactory work-around in the meantime? I doubt I will get around to removing this limitation in time for the release (Makarius is planning to branch off from development branch on Friday), but it's on my TODO list along with some wishes by Andreas Lochbihler.

since this is not the only problem in my formalization relying on
corecursion, I abandoned it for the time being.
I will have to rethink my overall approach.
So at the moment it is not very urgent.

> 
> Cheers,
> 
> Jasmin
> 

Thanks,
Tom




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