Re: [isabelle] quotient_type command fails
- To: Salomon Sickert <sickert at in.tum.de>
- Subject: Re: [isabelle] quotient_type command fails
- From: Makarius <makarius at sketis.net>
- Date: Tue, 1 Jul 2014 21:41:53 +0200 (CEST)
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Tue, 10 Jun 2014, Salomon Sickert wrote:
I guess this is the right place to report bugs. If not, please refer me to
the right place.
Apparently in Isabelle 2013-2 the quotient_type command doesn't work, if the
theory name contains white-space.
In my testcase the theory was called "With Whitespace" and the command
produced the following error:
attribute "Lifting.lifting_restore_internal": bad arguments
I attached a testcase for the problem to reproduce the issue. One theory
called "WithoutWhitespace.thy", which works fine, and a copy renamed to
"With Whitespace.thy", which fails.
The quotient_type command might have some weaknesses in its implementation
to break in such an odd way, but theory names with white-space just don't
make any sense. Think of it as a formal module name and a file-name at
the same time: use plain ASCII identifier syntax without any special
The canonical form without whitespace actually uses an underscore:
Without_Whitespace.thy -- camel case is not used in Isabelle sources (at
least not in up-to-date ones).
This archive was generated by a fusion of
Pipermail (Mailman edition) and