Re: [isabelle] Are unnamed theorems used by automatic methods or Sledgehammer?

On 8/27/2012 4:21 PM, Makarius wrote:

I don't think it would be a good idea to introduce aliases for existing commands, especially very short ones. If you want to be fast in typing it is better to figure out some jEdit plugins that do the job. The Sidekick completion is already there; it has some plugin options to make it more aggressive. Other plugins like superabbrevs or yet unknown ones might do even more for you.

It was only about style. Some keywords I like or don't mind, but "oops" and "sorry" don't quite fit in. It's not a problem because I don't think I'll be postponing or abandoning proofs much in the documents I give people, and I can strip some things out.

I was going to make a feeble appeal for freedom of keyword syntax, similar to how we have freedom of notation with Isar, but I decided it's the standardized keywords that give the language a common feel from document to document. If you were to let people redefine keywords, there would be major fragmentation of the language, which would make the language harder to learn, and you would get blamed for it.

Line noise that is hacked into the computer is better not stored in the text you produce, unless you never want anyone to read it, maintain it, work with it elsewise.

Some people have come up with proof languages based on single letter commands, or even non-letter commands in the spirit of APL. I am fond of typing fast, but not of reading what looks like mouse droppings on the screen.

Readability is huge with me, but it takes a lot of experimenting to find the balance between using brevity for clarity, and using verboseness for clarity.


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