[isabelle-dev] time specifications
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Tue Nov 2 17:23:32 CET 2010
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.
More information about the isabelle-dev