Re: [isabelle] Turning on tracing for mode inference?
The predicate compiler offers various tracing options that you can pass to the code_pred
command. (It is independent of the code generator, so the tracing settings for the code
generator do not apply.)
Here is a command that enables as much tracing as possible:
Just delete those options that you are not interested in. Probably you want to keep
Hope this helps,
On 10/11/16 10:06, Mark Wassell wrote:
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
I have tried
This archive was generated by a fusion of
Pipermail (Mailman edition) and