Re: [isabelle] No type arity itself

Hi Mark,

>    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)"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.