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



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

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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