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

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"
> 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

Attachment: OpenPGP_signature
Description: OpenPGP digital signature

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