[isabelle] How can I use Code_Abstract_Nat in Isabelle?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] How can I use Code_Abstract_Nat in Isabelle?
- From: Michael Stampone <michaelstampone at gmail.com>
- Date: Fri, 19 Nov 2021 00:14:19 -0500
- Authentication-results: cam.ac.uk; iprev=pass (mail-ed1-f43.google.com) smtp.remote-ip=184.108.40.206; spf=pass smtp.mailfrom=gmail.com; dkim=pass header.d=gmail.com header.s=20210112 header.a=rsa-sha256; arc=none
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"
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