Re: [isabelle] Rational numbers in Isabelle/ML



On Sat, 2 Apr 2016, Manuel Eberl wrote:

   * Option.map is the only canonical operation from that structure,
 everything else should be ignored.
All right, then what is the canonical way to do things like that? Nested case statements? Those can get very ugly and unreadable very fast.

There is nothing wrong with case expressions. Isabelle/ML is not as point-free as Haskell.

See also the "implementation" manual about "Options":

  Apart from @{ML Option.map} most other operations defined in structure
  @{ML_structure Option} are alien to Isabelle/ML and never used. The
  operations shown above are defined in @{file
  "~~/src/Pure/General/basics.ML"}.


Here is a general note from the manual about the basis library from NJ:

  The basis library proposal of SML97 needs to be treated with caution.
  Many of its operations simply do not fit with important Isabelle/ML
  conventions (like ``canonical argument order'', see
  \secref{sec:canonical-argument-order}), others cause problems with the
  parallel evaluation model of Isabelle/ML (such as @{ML TextIO.print} or
  @{ML OS.Process.system}).


	Makarius




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