Mark Wassell

2016-07-23 14:02:53 UTC

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

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