:( 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 >
