Post by Mark Wassell
let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card Basis"
the error is in this line. Roughly speaking, the type of "Basis" is too
general: it can be an arbitrary fresh 'b::euclidean_space, not the
'a::euclidean_space you in the previous line. The reason is that you
immediately apply the "card" function to it, which is of type "'a set =>
nat". So from the outside there is no indication which type is meant.
The system "helpfully" detects these situations and introduces an
explicit type parameter disguised as a value parameter.
You can observe this parameter when you print ?P:
"λtype b. LEAST N. ∀n≥N. dist (f b n) (g b) < r / real (card Basis)"
:: "'b itself ⇒ 'a ⇒ nat"
Luckily, the solution is simple: Just give a type annotation for "Basis":
let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card (Basis::'a set)"