Dear all,
while it is in principle nice that during Haskell code generation
do-blocks are mapped to Haskell do-blocks when using the heap monad of
Imperative HOL, it seems that the setup did not consider do-blocks as
arguments to functions. As a minimal example
theory Test
imports "~~/src/HOL/Imperative_HOL/Imperative_HOL"
begin
definition "foo m = do { m; return () }"
definition "bar = foo (do { return (); return () })"
export_code bar in Haskell
the code for "bar" does not compile, since parenthesis are missing
around its argument do-block.
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
