Am 02.11.2010 um 14:08 schrieb Makarius:
> The scheme of seconds as float addresses the intuition of at least 3 others
> on this thread, as well as Jasmin's requirement to re-scale numbers.
>
> It only makes sense to make this move, if we arrive at a single standard in
> the end, instead of four of them.
Floating-point numbers are a decent alternatives, and seconds, being the
standard unit for time in physics and elsewhere, makes sense; hence, I will not
stand in the way of standardization. (My personal preference does remain for a
unit suffix, e.g., "s", for readability's sake, though.)
A very minor issue is that I was never able to parse options like
nitpick [timeout = 1.5]
even with custom parsers, unless 1.5 is doubly-quoted. Users might not realize
they need quoting and will most probably be confused by the resulting error.
Jasmin
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
