[isabelle] Question about Code Generator


I have defined some datatype using typedef, it encapsulates some
data-structure together with its invariant, for example distinct lists
(used to implement sets here):

typedef 'a lset = "{ l::'a list . distinct l }"

  by auto

On this, I can define operations, e.g.:

definition "ls_empty == Abs_lset []"

definition "ls_\<alpha> l == set (Rep_lset l)"

definition "ls_memb x l == x mem (Rep_lset l)"

definition "ls_ins x l == if ls_memb x l then l else Abs_lset (x #
Rep_lset l)"


My question is, how to setup the code generator such that it implements "'a
lset" by "'a list", or, in general, in the same way as it would
implement the underlying datatype ?

With no further ado, the code generator complains about missing code

export_code ls_empty ls_memb ls_ins in SML file -

*** No code equations for Rep_lset, Abs_lset

*** At command "export_code".

Regards and thanks in advance for any help/pointers to examples

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