Re: [isabelle] Slots for diagnostic value command
I'd be in favour of re-introducing the slots. Among others, I have used "value [code]" to
automatically check the sanity of the code generator setup like a regession test.
On 31/07/14 09:48, Florian Haftmann wrote:
In 4044a7d1720f, there was a change: the ancient »slots« for value
(code, nbe, simp) and the default behaviour of sequential trys have been
given up in favour of one hard-coded behaviour:
* If the term to evaluate does not contain free variables, evaluate
* If the term contains free variables or the first step fails, evaluate
Recent experience suggests that this step was maybe too rigorous since
»value« is also used for purposes beyond diagnostic evaluation which
demand a more predictable behaviour, esp. wrt. ongoing developments of
My suggestion would be to revive the »slots« as follows:
* Slot »default« implementents the current behavior and is the default.
* The former slots (s.a.) are restored again.
This is something I definitely do not promote for the approaching
release, but rather for its successor.
This archive was generated by a fusion of
Pipermail (Mailman edition) and