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



Hi Andreas,

> It is hard to say what goes wrong here given that I do not know what
> your types in the signature of the inductive predicates are. From the
> error message, I guess that something goes wrong during the higher-order
> mode analysis in the predicate compiler.

as far as I can tell, there is no higher-order-ness involved.

> As a first step, I recommend to
> specify the modes for all predicates. The syntax looks as follows:
> 
> code_pred
>   (modes: evaluate_match: ... as ..
>       and evaluate_list: ... as ..
>       and evaluate: ... as ..)
>   evaluate .

This gives an even lower-level error:

> exception THM 1 raised (line 332 of "drule.ML"):
>   RSN: no unifiers
>   xh  [xh]
>   ?s = ?t ⟹ ?t = ?s

I have attached a self-contained zip file. The problematic invocation is
in "Scratch.thy", which should be loaded with the "CakeML" image (see ROOT).

Cheers
Lars

Attachment: cakeml_bigstep.zip
Description: Zip compressed data



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