On 03.09.2013 16:21, Makarius wrote:
On Tue, 3 Sep 2013, Lawrence Paulson wrote:
For sure. I think it confuses beginners at first, because == is only
allowed in "real" definitions rather than derived ones.
"Real" definitions are actually just for foundational purposes: users
never see them --
On Tue, 3 Sep 2013, Lars Noschinski wrote:
On 03.09.2013 16:21, Makarius wrote:
On Tue, 3 Sep 2013, Lawrence Paulson wrote:
For sure. I think it confuses beginners at first, because == is only
allowed in "real" definitions rather than derived ones.
"Real" definitions are actually just for f
On Tue, 3 Sep 2013, Lawrence Paulson wrote:
For sure. I think it confuses beginners at first, because == is only
allowed in "real" definitions rather than derived ones.
"Real" definitions are actually just for foundational purposes: users
never see them -- neither end-users nor users in the s
For sure. I think it confuses beginners at first, because == is only allowed in
"real" definitions rather than derived ones.
Larry
On 3 Sep 2013, at 00:39, Gerwin Klein wrote:
> I also still use == quite a bit, I never understood why it is discouraged so
> much. It has the better precedence, a
Almost always I use <-->. The only exception being a comparison of
booleans, like in "if (a::bool) = b then ..."
-- Peter
On Di, 2013-09-03 at 09:33 +0900, Christian Sternagel wrote:
> Same here. - cheers chris
>
> Florian Haftmann wrote:
>
> >> Are there clubs of "iff" vs. "non-iff"? If alm
Same here. - cheers chris
Florian Haftmann wrote:
>> Are there clubs of "iff" vs. "non-iff"? If almost everybody is a member
>> of the "iff" club we could just remove that print mode. (We don't have
>> to consider that for the coming release, to avoid any real-time pressure
>> on this question
On 03/09/2013, at 12:24 AM, Makarius wrote:
> Are there clubs of "iff" vs. "non-iff"? If almost everybody is a member of
> the "iff" club we could just remove that print mode. (We don't have to
> consider that for the coming release, to avoid any real-time pressure on this
> question.)
I l
To me, the ability to use = (on booleans) as an alternative to <-> is an
artefact of HOL, rather than something to encourage. Almost always, <-> is more
readable. At least that's my view.
Larry
On 2 Sep 2013, at 19:42, Florian Haftmann
wrote:
>> Are there clubs of "iff" vs. "non-iff"? If al
> Are there clubs of "iff" vs. "non-iff"? If almost everybody is a member
> of the "iff" club we could just remove that print mode. (We don't have
> to consider that for the coming release, to avoid any real-time pressure
> on this question.)
I am definitely a member of the iff-club. Partly for
On Mon, 2 Sep 2013, Makarius wrote:
I find myself using the "iff" notation most of the time to make theories
look "nice".
Are there clubs of "iff" vs. "non-iff"? If almost everybody is a member of
the "iff" club we could just remove that print mode.
I've forgotten to point out the relation
On Mon, 2 Sep 2013, Lawrence Paulson wrote:
I tend to use <->, but I'm afraid I don't know what a print mode is.
A print mode allows to change the way how the system prints things; there
are command line options -m MODE or Isabelle settings to various isabelle
tools for that.
Sometimes pri
I tend to use <->, but I'm afraid I don't know what a print mode is.
Larry
On 2 Sep 2013, at 15:29, Tobias Nipkow wrote:
> For uniformity I almost always use "=" and would not like to see it printed
> as <-->.
>
> Tobias
>
> Am 02/09/2013 16:24, schrieb Makarius:
>> (This is just a side-track
For uniformity I almost always use "=" and would not like to see it printed as
<-->.
Tobias
Am 02/09/2013 16:24, schrieb Makarius:
> (This is just a side-track on HOL notation, which came to me when cleaning up
> theories with old ASCII replacement syntax like & | --> <-> Un Int etc. --
> which
(This is just a side-track on HOL notation, which came to me when cleaning
up theories with old ASCII replacement syntax like & | --> <-> Un Int etc.
-- which is very easy with explicit C+b completion in Isabelle/jEdit.)
Isabelle/4379d46c8e13 (Oct 2005) introduces "alternative iff syntax for
e
14 matches
Mail list logo
