[isabelle] Fixing modes for all predicates in mutually recursive block when using code_pred
I am finding that mode checking on a block of mutually recursive predicates
is taking a long time (5+ minutes) and this is hindering any sort of
I know the mode I want for each predicate in the block and although I can
fix the mode for one of the predicates in the code_pred command, it looks
like all modes are being checked for the other predicates.
Is there a way to fix the modes for all of the predicates so that the mode
checking doesn't waste time exploring modes I have no interest in?
This archive was generated by a fusion of
Pipermail (Mailman edition) and