[isabelle-dev] instantiation

[Amine Chaieb]

:( I also failed a few weeks ago to instantiate the fold combinator to 
iterate function composition ...

But is this restriction fundamental or does it happen to be there?

Amine.

Florian Haftmann wrote:
> Amine Chaieb schrieb:
>> Dear all,
>>
>> (How) Can I perform an instantiation of a type-constructor with two
>> arguments, an thereby restricting them to be the same?
> 
> This is beyond the type class system of Isabelle.  A pity.
> 
> 	Florian
>