Email Gateway (Aug 19 2022 at 14:56): Email Gateway (Aug 19 2022 at 14:56):From: Joachim Breitner <breitner@kit.edu>
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
signature.asc
Email Gateway (Aug 19 2022 at 14:56):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, that is a message from the internals of list comprehension and has
always been there.
Tobias
Last updated: Apr 24 2024 at 20:16 UTC