On 05/30/2011 06:03 PM, Lukas Bulwahn wrote:
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
defi
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where "test xs = (last xs = 0)"
de
Hi Lukas,
here is an example that I would have expected to work. However, congruences seem
to work other than I expected. Du you know what I am missing here?
theory Scratch imports Main begin
definition test where "test xs = (last xs = 0)"
definition test2 where "test2 xs = (xs ~= [] & test (r
On 05/30/2011 10:31 AM, Andreas Lochbihler wrote:
Thanks Lukas and Florian.
I guess that it *is* a corner case in my specifications, because I
have a conditional code equation that implements one constant x in
terms of another y. However, I use x only in the equation of another
constant z whi
Thanks Lukas and Florian.
I guess that it *is* a corner case in my specifications, because I have a
conditional code equation that implements one constant x in terms of another y.
However, I use x only in the equation of another constant z which tests for the
precondition first. At the moment,
Hi Andreas,
the following ML line should do the job of adding the congruence rule in
your case:
setup {* Code_Preproc.map_pre (fn ss => ss addcongs [@{thm conj_cong}]) *}
Before we add yet another feature to the code generation setup in Isar,
we would like to understand your scenario.
Does
Does the current attribute mechanism support selective attributes such
as [code_inline cong], maybe along the lines of [simp del]? If it does,
I assume it would be easy to add that information in the place that
Florian pointed to?
Tobias
Am 28/05/2011 14:45, schrieb Florian Haftmann:
Hi Andr