Re: [isabelle] pairs and friends



I see. Have a nice vacation. I will try to figure something out.
Thanks,
Tom

On 09/30/2016 12:45 PM, 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
> 
> I'm on vacation for two weeks starting today and won't be able to look into this until then. I hope we can support your function. In any case, the error message is wrong. Hopefully, you can either wait until then or find a workaround.
> 
> Cheers,
> 
> Jasmin
> 




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