Re: [isabelle] Isabelle style guide - Part 2

On Sat, 30 May 2015, Gerwin Klein wrote:

As promised, part 2 of the Isabelle style guide:

Feedback for the first part was great, keep it coming!

* "Isabelle supports literal proofs": you probably mean "literate proofs".
  This should give most people an idea about the point of it, although the
  official slogan talks about "proof documents".

  You could also add a note that the SideKick plugin of Isabelle/jEdit
  helps getting an overview of a text that is nicely structured with
  chapter, section, subsection etc.

* CamelCaseNames for datatype constructors: around 2006/2007 this was
  discontinued as canonical form in Isabelle/Pure/ML and replaced by
  Camel_Case_Names with_proper_underscore.  Both the old and new forms are
  widely used, though, since renaming constructors in ML is always a bit
  dangerous (but not in HOL).

* About bad "definition f" and "This will reserve the name f and make it
  unusable for variables".  Having a constant called "f" in the global
  context is certainly bad, but there should always be a way to produce a
  free variable of that name, by using explicit "fixes", "for"  or "!!f.
  ..." in closed propositions.  Isar has been designed like that from the
  very start, although surprisingly many people don't know that --
  especially when building tools that ignore the concepts of
  eigen-contexts of statements.

* "typed as \open and \close in jEdit": This should be Isabelle/jEdit,
  since jEdit does not know anything about it.  The canonical shortcut in
  the Prover IDE works via ASCII backquote, although that is sometimes
  hard to find on strange keyboards (e.g. German Macintosh).  At some
  point, the canonical key for cartouches might become " (double-quote),
  when terms are accepted in that form as well.


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