+get-first : (a : Type) => (b : Type) => Pair -> a; +get-second : (a : Type) => (b : Type) => Pair -> b;
^^^^ Pair a b et les arguments a et b peuvent être erasable plutôt que seulement implicites.
+get-x : (a : Type) => Point -> a; +get-y : (a : Type) => Point -> a;
^^^^^ Point a même chose ici pour a
Stefan