Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] function evaluation in ML

view this post on Zulip Email Gateway (Aug 18 2022 at 14:15):

From: Kamil Kubon <kamil.kubon@gmail.com>
Hello,

I want to ask you, if there is some way to
use "value" or "normal_form" or some similar construct directly in ML{..}.

I just want to call function (with string result) defined in
Isabelle/Isar from ML ,
and store that result in file..

Thanks for any suggestions.

Kamil.

view this post on Zulip Email Gateway (Aug 18 2022 at 14:17):

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

I want to ask you, if there is some way to
use "value" or "normal_form" or some similar construct directly in ML{..}.

Value.value seems to be what you want.

See further ML module src/Tools/value.ML in the Isabelle distribution.

Hope this helps
Florian
signature.asc

Last updated: Apr 23 2024 at 12:29 UTC