Email Gateway (Aug 22 2022 at 13:50): Email Gateway (Aug 22 2022 at 13:50):From: Mark Wassell <mpwassell@gmail.com>
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
Email Gateway (Aug 22 2022 at 13:50):From: Lars Hupel <hupel@in.tum.de>
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)"
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:50):From: Mark Wassell <mpwassell@gmail.com>
Lars,
Thank you for your comprehensive answer. One small question: How do I
print ?P ?
Mark
Email Gateway (Aug 22 2022 at 13:50):From: Manuel Eberl <eberlm@in.tum.de>
term "?P"
Last updated: Apr 20 2024 at 08:16 UTC