[isabelle] Turning on tracing for mode inference?
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