Re: [isabelle] How can I use Code_Abstract_Nat in Isabelle?


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.


On 19/11/2021 12:03, Florian Haftmann wrote:
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.


Am 19.11.21 um 06:14 schrieb Michael Stampone:
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"

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.