Re: [isabelle] pairs and friends



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.