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