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:
> (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)
> 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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and