[isabelle] No type arity itself
With the following:
fix f :: "'a::euclidean_space â nat â real" and g::"'a::euclidean_space
let ?P = "Îb. LEAST N. ânâN. dist (f b n) (g b) < r/ card Basis"
let ?Q = "Max ( ?P ` Basis)"
I get the error "No type arity itself :: euclidean_space" at the "let ?Q"
Can anyone tell me what 'itself' is and how to resolve this problem?
This archive was generated by a fusion of
Pipermail (Mailman edition) and