[isabelle] No type arity itself



Hello,

With the following:

notepad
begin
   fix r::real
   fix f :: "'a::euclidean_space â nat â real" and g::"'a::euclidean_space
â real"

   let ?P = "Îb. LEAST N. ânâN. dist (f b n) (g b) < r/ card Basis"
   let ?Q = "Max ( ?P ` Basis)"
end

I get the error "No type arity itself :: euclidean_space" at the "let ?Q"
statement.

Can anyone tell me what 'itself' is and how to resolve this problem?

Cheers

Mark



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