[isabelle] Turning on tracing for mode inference?



Hello,

I have an inductive relation that I am attempting to generate code for.
It's a reduction relation:

reduce :: "e â store â e â store â bool"

I believe that there is one rule that is preventing mode inference from
deriving any functions (ie things like reduce_i_i_i_i)

Is there a way to turn on tracing here? I see in the ML code lines that
look like they would output trace information but have had no luck enabling
the trace.

I have tried

declare [[code_runtime_trace=true,code_simp_trace=true]]

Cheers

Mark



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.