On Thu, 27 Aug 2015, Florian Haftmann wrote:
*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the source-level debugger of Poly/ML, to work with
Isabelle/ML and official Standard ML.
That's a promising announcement.
However I struggle to get something run from the attached
The situation of the screenshot looks OK so far. Now you should
activate the fun*loop breakpoint via the context menu of jEdit -- it
requires some practice to get the mouse position right. Then you can
scroll further down to run some ML_val snippets, or produce dummy edits
to ensure they
Hi Dmitriy,
thanks for your answer.
Let me rephrase the matter as I perceive it:
Syntactic requirement: Print and parse singleton case clauses as let
bindings.
I agree that this can (and should) be done in a separate phase. Still
not sure whether check/uncheck is the right layer to accomplish
Currently, we have two simplifier tracing implementations, the classical
one and the »new« one, which according to isar-ref still presents itself
as a non-replacing alternative.
What are the plans to continue from there? This also affects derived
functionality like tracing of code equation
Hi Dmitriy,
In short, I have come to the conclusion that
let (a, b) = p in t
case p of (a, b) = t
at the moment being logically distinct, should be one and the same. In
other words, I suggest that any case expression on tuples should be
printed using »let« rather than »case«.
