[isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode

Tobias Nipkow nipkow at in.tum.de
Wed Jul 6 13:48:55 CEST 2011

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.


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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list