Re: [isabelle] pairs and friends



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.