[isabelle-dev] instantiation
Amine Chaieb
ac638 at cam.ac.uk
Mon Oct 27 17:03:07 CET 2008
:( 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
>
More information about the isabelle-dev
mailing list