[isabelle] Question about Code Generator



Hi,

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
equations:

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
  Peter









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