Re: [isabelle] value [code] raises Match in code_ml.ML

> Abstract datatypes are a good idea, and it is possible in my case. I can
> also get rid of the code_const for the abstraction function (Abs_foo for
> the typedef, Foo in the original example). Unfortunately, I am then
> stuck with the representation function Rep_foo, for example
> definition test where "test = Rep_foo bar"
> If I declare a code equation for Rep_foo, code generation works for
> test, but code_simp loops.

I am not sure whether I understand properly.  If Abs_foo is an abstract
constructor, the code equation

  Rep_foo (Abs_foo x) = x

is implicit.  I admit the system allows, pointlessly, to override this,
but this should be considered a feature aka bug.  So what is your exact



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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