Re: [isabelle] Predicate compiler: mode and term do not match



> I don't know either what it is that triggers this exception, but I
> suspect that it has something to do with all those tuples in your types.

I'm afraid I can't change these definitions; this is code which is being
automatically generated by Lem from the CakeML sources.

> However, for values, you also have to do the termination proofs for the
> functions pmatch, do_eq and pat_bindings. In summary, the following
> works in Isabelle2013-2:
> 
> code_pred
>   (modes: evaluate:       i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool
>       and evaluate_list:  i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool
>       and evaluate_match: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool)
>   [skip_proof]
>   evaluate .
> 
> termination pmatch by lexicographic_order
> termination do_eq by lexicographic_order
> termination pat_bindings by lexicographic_order

Great, that works like a charm. In the end, I'm probably not going to
need the code setup, but it might be worth investigating anyway why this
fails. I don't see any special things going on here.

Thanks for your help!
Lars




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