Re: [isabelle] Floor and ceiling

On Thu, 21 Aug 2014, W. Douglas Maurer wrote:

I am using Isabelle 2013-2. I was trying to use the floor symbols from the Symbols window. Looking at \<lfloor> under Punctuation, I see abbrev: [. Looking at \<rfloor>, I see abbrev: .] So the floor of x, then, should be [. x .] But then I looked at the ceiling symbols. Looking at \<lceil>, I see abbrev: [. Looking at \<rceil>, I see abbrev: .] So the ceiling of x, then, should also be [. x .] This can't be right. What is [. x .] ? Is it floor(x) or is it ceiling(x)? Or has this already been fixed in the 2014 edition?

There is nothing broken and nothing to be fixed here, merely a misunderstanding of what symbol abbreviations are. See also the Isabelle/jEdit manual page 16:

  Note that the above abbreviations refer to the input method. The logical
  notation provides ASCII alternatives that often coincide, but deviate
  occasionally. This occasionally causes user confusion with very
  old-fashioned Isabelle source that use ASCII replacement notation like !
  or ALL directly in the text.

There is more text around it that talks about input methods for Isabelle symbols. You don't write any ASCII abbreviations in the final text, and [. x .] is invalid in the normal term syntax anyway.

In Isabelle2014 the Isabelle/jEdit manual is once again longer and more thorough, and the input mechanisms have been refined as well.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.