[isabelle] What do the predicate compilation options such as inductify and random_dseq do?



Hello,

In Predicate_Compile_Examples/Examples.thy there are the following uses of
code_pred and value:

code_pred [inductify] Sâ1p .
code_pred [random_dseq inductify] Sâ1p .

values [random_dseq 5, 5, 5] 5 "{x. Sâ1p x}"

Is there any detailed documentation or description of what the compilation
options such as inductify and random_dseq do? Or will I need to read the ML
?

What I can tell from the equation lines is that these options result in
different code equations with the latter possibly enabling random
generation of the members of the inductive set in a quickcheck like manner.

Cheers

Mark



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