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)"
 
Larry

> 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 MHonArc.