Re: [isabelle] quotient_type command fails

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 ambitions.

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 MHonArc.