Re: [isabelle] find_theorems and locales
We clearly need to look at how type inference affects find_theorems.
The missing at sea (dist_norm) belongs to the type class of the same name, of which real_normed_vector is a subclass. It seems obvious that the pattern "_ = norm (_ - _)â should pick up
dist_norm: "dist x y = norm (x - y)"
> On 25 Jun 2015, at 15:50, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> It seems to be a constraint issue:
> find_theorems "_ = norm (_ - _)"
> ~> 'a::real_normed_vector is inferred
> find_theorems "_ = norm ((_::'a::dist_norm) - _)"
> ~> typing error
> Maybe some naughty tweaking of sort constraints or an unforseen
> behaviour of coercions, but these are mere guesses. I do not understand
> these parts of the type class hierarchy.
This archive was generated by a fusion of
Pipermail (Mailman edition) and