Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Implizite type-parameter und partiell angewandte Funktion
Ich habe folgendes Problem:
Ich habe eine Funktion , die einen Typparameter hat "bla {A : type} A → A → Real "
Jetzt kann ich den Typparameter durch so etwas wie “# blabla 2 3” umgehen. Dann habe ich allerdings das Problem , dass ich immer den 2. und 3. Parameter angeben muss , wenn ich “blabla” verwende.
Was ich will ist, dass ich den Typparameter (das “{A : type}”) implizit machen kann , und zugleich die Funktion sich “curried” verhält (ich also nicht immer alle Parameter gleichzeitig angeben muss).
Z.B. sollte folgendes möglich sein : [x : nat] bla x
Edit:
Zusätsliche Frage (nur aus eigenem Interesse ) : gibt es schon etwas mehr zu Category-Theory ? (habe nur in smglom was zu altes gefunden “categories_old.mmtxx”)
“# blabla 2” sollte genau das tun 
alternativ “# blabla %I1”.
In ersterem Falle erfordert die Notation “nur” das zweite Argument (womit das erste implizit ist); der return type wird damit A → Real. Im zweiteren Falle wird direkt nur das erste argument als implizit markiert, der verbleibende typ von blabla wäre also A → A → Real, was entsprechend auf’s selbe rausläuft