Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] value command failed

view this post on Zulip Email Gateway (Mar 09 2022 at 10:47):

From: Tobias Nipkow <nipkow@in.tum.de>
If the "value" command fails with a compilation error

(At (line 139 of "generated code")
Exception- Fail "Static Errors" raised)

is there any way to look at the code? Note: if I turn the offending expression
into a definition and export that code, there is no problem, so something is
special about "value".

Tobias
smime.p7s

view this post on Zulip Email Gateway (Mar 09 2022 at 11:00):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
declare [[code_runtime_trace]]

should do the job.

Florian
OpenPGP_signature

Last updated: Jul 15 2022 at 23:21 UTC