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
setup?

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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