Re: [isabelle-dev] NEWS: op -> ()

On 06/03/18 16:04, Peter Lammich wrote: > I observed that "(=)" is hard to type in the default symbols setup, it > will be folded to "\)" if immediate completion is on (A short > informal poll in our group resulted that most of us have immediate > completion on). Of course, the default setup

Re: [isabelle-dev] NEWS: op -> ()

I observed that "(=)" is hard to type in the default symbols setup, it will be folded to "\)" if immediate completion is on (A short informal poll in our group resulted that most of us have immediate completion on). When trying to write parametricity lemmas in predicate-style (eg for

Re: [isabelle-dev] NEWS: op -> ()

I'd prefer to keep things simple. I do like your recent syntactic innovations, but such things need to be introduced with care. And the inner syntax is considerably more delicate. Larry > On 2 Feb 2018, at 10:50, Makarius wrote: > > The general concept behind it is

Re: [isabelle-dev] NEWS: op -> ()

On 01/02/18 17:23, Tobias Nipkow wrote: > > I think (simple) sections do indeed improve readbility. BUT in the light > of your comments I am not keen on them in Isabelle. We do not need yet > more syntactic sugar. For the record, here are a few more questions: >> Here are also some notes from

Re: [isabelle-dev] NEWS: op -> ()

Happy to agree Larry > On 1 Feb 2018, at 16:23, Tobias Nipkow wrote: > > I think (simple) sections do indeed improve readbility. BUT in the light of > your comments I am not keen on them in Isabelle. signature.asc Description: Message signed with OpenPGP

Re: [isabelle-dev] NEWS: op -> ()

Makarius, I think (simple) sections do indeed improve readbility. BUT in the light of your comments I am not keen on them in Isabelle. We do not need yet more syntactic sugar. Thanks Tobias On 01/02/2018 16:41, Makarius wrote: On 01/02/18 07:41, Tobias Nipkow wrote: At the time I was also

Re: [isabelle-dev] NEWS: op -> ()

On 01/02/18 07:41, Tobias Nipkow wrote: > > At the time I was also wondering whether to allow `sections', eg "(+ 1)" > or (1 +)" but did not want to overdo it. It sounds like that at least > with your parser imporvements it might be ok? I am unsure -- my changes barely recovered the old

Re: [isabelle-dev] NEWS: op -> ()

I was afraid of exactly this when I made the change but only looked at the build times for the distribution (which seemed fine) but not the AFP. Thank you for spotting and even undoing the performance regression. I look forward to having (*) in the inner syntax. At the time I was also

Re: [isabelle-dev] NEWS: op -> ()

On 10/01/18 20:17, Tobias Nipkow wrote: > * The "op " syntax for infix operators has been replaced by > "()". If begins or ends with a "*", there needs to > be a space between the "*" and the corresponding parenthesis. > > In revision eab6ce8368fa That change actually had significant

Re: [isabelle-dev] NEWS: op -> ()

Thanks for this discussion. Although I agree with Larry and Andreas, it is clear that there is no concensus. Hence there will be no blanket change of where line breaks go for infix operators. Tobias On 16/01/2018 17:34, Blanchette, J.C. wrote: This sort of claim needs to be justified by

Re: [isabelle-dev] NEWS: op -> ()

On Di, 2018-01-16 at 16:31 +, Lawrence Paulson wrote: > I know how to do it, but no beginner could ever find this. > Larry This is usually one of the first things I show students learning Isabelle ... I'm using brackets syntax in demos, but let  them decide which syntax they like better. Peter

Re: [isabelle-dev] NEWS: op -> ()

> This sort of claim needs to be justified by evidence. We had it the first way > until the late 1990s. I changed it to the other way while working on large > proof states connected with crypto protocols. It seemed more readable to me > for such proofs. I was taught at school to avoid

Re: [isabelle-dev] NEWS: op -> ()

I know how to do it, but no beginner could ever find this. Larry > On 16 Jan 2018, at 16:20, Andreas Lochbihler > wrote: > > It's not too hard: Go to Plugins/Plugin Options/Isabelle/General and enter > "brackets" under Print mode.

Re: [isabelle-dev] NEWS: op -> ()

On 16/01/18 16:14, Lawrence Paulson wrote: On 16 Jan 2018, at 14:13, Blanchette, J.C. wrote: However, for operators like ==>, which bind on the right, foo ==> bar is actually much more readable than foo ==> bar This sort of claim needs

Re: [isabelle-dev] NEWS: op -> ()

> On 16 Jan 2018, at 14:13, Blanchette, J.C. wrote: > > However, for operators like ==>, which bind on the right, > > foo ==> > bar > > is actually much more readable than > > foo > ==> bar This sort of claim needs to be justified by evidence. We

Re: [isabelle-dev] NEWS: op -> ()

> On 11 Jan 2018, at 16:44, Tobias Nipkow wrote: > > There are a number of different points here. > > - What is good style depends on what your math look like. Knuth writes nice > traditional math, whereas Isabelle proof states can get quite ugly. In such > cases I find that

Re: [isabelle-dev] NEWS: op -> ()

On 11/01/2018 14:10, Makarius wrote: On 10/01/18 21:46, Tobias Nipkow wrote: I seem to remember Lamport makes a similar point but it is not in his "How to write a proof".] The paper is called "How to Write a Long Formula" and available e.g. here:

Re: [isabelle-dev] NEWS: op -> ()

There are a number of different points here. - What is good style depends on what your math look like. Knuth writes nice traditional math, whereas Isabelle proof states can get quite ugly. In such cases I find that operator names on the next line improves readability, independent of what the

Re: [isabelle-dev] NEWS: op -> ()

On 10/01/18 20:17, Tobias Nipkow wrote: > Invoking "isabelle update_op" converts all files in the current directory > (recursively). > In case you want to exclude conversion of ML files (because the tool > frequently also converts ML's "op" syntax), use option "-m". I've made some minor

Re: [isabelle-dev] NEWS: op -> ()

On 11/01/18 13:20, Lawrence Paulson wrote: >> On 10 Jan 2018, at 21:26, Makarius wrote: > > Interactive theorem proving isn't the same thing as solving physics problems > by hand, so I'm not against having operators at the end of the line if that's > what people think

Re: [isabelle-dev] NEWS: op -> ()

On 10/01/18 21:46, Tobias Nipkow wrote: > > I seem to remember Lamport makes a > similar point but it is not in his "How to write a proof".] The paper is called "How to Write a Long Formula" and available e.g. here: https://lamport.azurewebsites.net/pubs/lamport-howtowrite.ps.Z In the early

Re: [isabelle-dev] NEWS: op -> ()

> On 10 Jan 2018, at 21:26, Makarius wrote: > > The Haskell community appears to have picked up a lot of such (slightly > odd) styles from Lamport. E.g. they put commas at the start of the line > instead of the end, which is typographically very strange. > > I was educated

Re: [isabelle-dev] NEWS: op -> ()

On 10/01/18 21:46, Tobias Nipkow wrote: > > Having the operator on the new line in case > of a break makes a lot of sense to me because it clearly how this line > is connected with the previous one. [I seem to remember Lamport makes a > similar point but it is not in his "How to write a proof".]

Re: [isabelle-dev] NEWS: op -> ()

On 10/01/2018 21:23, Makarius wrote: On 10/01/18 20:17, Tobias Nipkow wrote: Invoking "isabelle update_op" converts all files in the current directory (recursively). In case you want to exclude conversion of ML files (because the tool frequently also converts ML's "op" syntax), use option

Re: [isabelle-dev] NEWS: op -> ()

On 10/01/18 20:17, Tobias Nipkow wrote: > Invoking "isabelle > update_op" converts all files in the current directory (recursively). > In case you want to exclude conversion of ML files (because the tool > frequently also converts ML's "op" syntax), use option "-m". > > In revision eab6ce8368fa

[isabelle-dev] NEWS: op -> ()

* The "op " syntax for infix operators has been replaced by "()". If begins or ends with a "*", there needs to be a space between the "*" and the corresponding parenthesis. INCOMPATIBILITY. There is an Isabelle tool "update_op" that converts theory and ML files to the new syntax. Because it is