Re: [isabelle] No type arity itself
Thank you for your comprehensive answer. One small question: How do I
print ?P ?
On 23-Jul-16 4:24 PM, Lars Hupel wrote:
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