That email talks about recursion through records in datatype definitions. That is not what this thread is about. Here we were talking about pattern matching only.
Tobias Am 06/07/2011 11:09, schrieb Makarius: > On Tue, 5 Jul 2011, Tobias Nipkow wrote: > >> I agree with Gerwin. Records are datatypes. Hence one should be able >> to pattern match against them as in FP languages. > > See also > https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2006-December/msg00000.html > > as an arbitrary point in the really long history of these highly complex > packages. > > >> The record package can arrange for this very easily via rep_datatype. > > No. It will involve much more things that were not even touched in the > discussion yet. > > > Makarius > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
