Email Gateway (Nov 19 2021 at 10:13): Email Gateway (Nov 19 2021 at 10:13):From: Michael Stampone <michaelstampone@gmail.com>
I would like to learn how to use function transformers in Isabelle. I tried
to make this minimal example and it didn't work, maybe I'm missing
something obvious. Please help me get this example to run so I can
understand Isabelle better.
theory Scratch imports Main "~~/src/HOL/Library/Code_Abstract_Nat"
begin
primrec f :: "nat ⇒ nat" where
"f 0 = 0"
| "f (Suc x) = f x"
declare [[show_types]]
code_thms f
I get an error message on the last line which says
No content for theory certificate HOL.Nat
Eventually, I would like to also
export_code f in SML module_name Whatever
Email Gateway (Nov 19 2021 at 11:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Michael,
which Isabelle release do you use?
Currently, there are a couple of RCs for the upcoming release, so this
is an important information to investigate your issue.
Cheers,
Florian
OpenPGP_signature
Email Gateway (Nov 19 2021 at 15:52):From: Manuel Eberl <manuel@pruvisto.org>
Hello,
I think you really want to import "HOL-Library.Code_Target_Numeral"
instead of what you imported. It seems to work with that.
Side note: importing things with "~~/src/HOL/…" is somewhat
old-fashioned and can lead to problems. It's not the problem here, but
still. Using the session-qualified import (as above) is better.
Manuel
Last updated: Jul 15 2022 at 23:21 UTC