Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation for sets (in the development v...

Email Gateway (Aug 18 2022 at 19:04):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lukas,

export_code List.map_project Set.union in SML file -

bad luck. List.map_project would fit best in Set.thy, but there is no
option type yet. It could be moved to Option.thy, but then the same
problem occurs with Option.set.

No idea the the moment…

Florian
signature.asc

Email Gateway (Aug 18 2022 at 19:15):

From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi all,

on a fairly recent development version of Isabelle (bd03e0890699), I
cannot generate code for sets due a module dependency cycle.

The problem boils down to:

export_code List.map_project Set.union in SML file -

Any suggestions how to avoid it or fix it?

By the way, code generation for sets now works nicely (besides this
error). Thanks, Florian. Keep up the work!

Lukas

Last updated: Apr 19 2024 at 20:15 UTC