Re: [isabelle] Fixing modes for all predicates in mutually recursive block when using code_pred



Yes it is and thank you.

Mark

On Sun, 14 Apr 2019 at 10:19, Andreas Lochbihler <mail at andreas-lochbihler.de>
wrote:

> Dear Mark,
>
> You can specify the modes for each predicate with the code_pred command.
> The syntax is as
> follows:
>
> Given two mutually recursive predicates
>
> inductive P1 :: "... => bool"
>    and P2 :: "... => bool" where ...
>
> you can write
>
> code_pred (modes: P1: i => ... => o => bool and P2: o => ... => i => bool)
> P1
>
> and the predicate compiler should no longer try all possible modes for P2.
>
> Is this what you are looking for?
>
> Best,
> Andreas
>
> On 13/04/2019 16:58, Mark Wassell wrote:
> > Hello,
> >
> > 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
> > iterative development.
> >
> > 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?
> >
> > Cheers
> >
> > Mark
> >
>



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