Re: [isabelle] pairs and friends



Thanks for the tip, Dmitriy. I will try it.

Cheers,
Tom

On 09/30/2016 04:17 PM, Dmitriy Traytel wrote:
> Hi Tom,
> 
> an admittedly ugly temporary workaround is to use a separate codatatype for streams of pairs:
> 
> codatatype 'a pairstream = SCons (shd: "'a à 'a") (stl: "'a pairstreamâ)
> 
> corecursive (friend) foo :: "'a list â 'a pairstream â 'a pairstream" where
>   "foo us T = (case us of
>     [] â SCons (shd T) (stl T)
>   | u # us â SCons (shd T) (stl T))"
>   unfolding relator_eq[symmetric] by transfer_prover
> 
> Cheers,
> Dmitriy
> 
>> On 30 Sep 2016, at 12:45, Jasmin Blanchette <jasmin.blanchette at inria.fr> 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.