Re: [isabelle] The following clauses are redundant (covered by preceding clauses)



Thanks, that is a message from the internals of list comprehension and has
always been there.

Tobias

On 17/07/2014 15:27, Joachim Breitner wrote:
> Hi,
> 
> I just found this (2014-RC0, maybe also in earlier versions):
> 
> definition foo :: "('a × 'b) list ⇒ ('a × 'b) list" where "foo Γ = [ (x, e)
> . (x,e) ← Γ]"
> 
> prints
> 
> The following clauses are redundant (covered by preceding clauses): x ⇒ []
> 
> 
> Greetings, Joachim
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.