Re: [isabelle] 2014-RC1 issues



On 30.07.2014 22:25, Makarius wrote:
> On Wed, 30 Jul 2014, Lars Noschinski wrote:
>
>> BTW: I always use(d) "error """ the way one uses "undefined" in Haskell.
>> The following construct (which Makarius showed me at ITP) is a bit nicer
>> (you get a trace and can jump to the location of the error), but
>> requires a few lines of initial setup:
>>
>> signature UTIL = sig
>>  exception Undefined
>>  val setup : theory -> theory
>> end
>>
>> structure Util : UTIL = struct
>>
>> exception Undefined
>>
>> val setup =
>>  ML_Antiquotation.inline @{binding undef} (Scan.succeed "raise
>> Util.Undefined")
>>  #> ML_Antiquotation.inline @{binding fundef} (Scan.succeed "fn _ =>
>> raise Util.Undefined")
>>
>> end
>
> After that ITP session, I recalled the more basic "raise Match" idiom,
> but could not tell you about it.  That is sufficiently short to be
> used literally.
When writing more then a few lines of code, I prefer a separate
"undefined" value -- "raise Match" has a double meaning as telling the
compiler not to bother me with warnings about inexhaustive cases.

  -- Lars




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