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.
On 17/07/2014 15:27, Joachim Breitner wrote:
> 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) ← Γ]"
> The following clauses are redundant (covered by preceding clauses): x ⇒ 
> Greetings, Joachim
This archive was generated by a fusion of
Pipermail (Mailman edition) and