Re: [isabelle] What do the predicate compilation options such as inductify and random_dseq do?
On 31/07/17 11:11, Mark Wassell wrote:
My general interest is understand in detail how the code generation for inductive
predicates works. My specific interest in random_dseq is in being able to randomly
generate terms in a language from its inductive definition (for example terms of a
particular type) and to do so in a manner where I have some control over the distribution.
I was wondering if the options to random_dseq in the values statement provided this
control or similar.
Sorry, I cannot help you here. I've never used those smart generators.
I have read "Code Generation from Inductive Predicates in Isabelle/HOL" March 2009, Lukas
Bulwahn. Is this the PhD thesis that you refer to?
No. This is the Lukas' Master's thesis on the predicate compiler. It contains a few more
details about the predicate compiler, but not the integration with quickcheck. Lukas' PhD
thesis is available here:
All the best,
This archive was generated by a fusion of
Pipermail (Mailman edition) and