Alex Weisberger (Sep 12 2022 at 01:43): Alex Weisberger (Sep 12 2022 at 01:43):I've started to play around with code generation, targeting OCaml for now. When I export a function with a nat argument, I'm only able to use that function by building up a nat value manually, e.g. Suc (Suc (Suc Zero_nat)).
Is there any trick to being able to use numerals directly?
Seung Hoon Park (Sep 13 2022 at 08:37):I have also been looking on how to do this a while ago. Have a look at section 7.3 of Code generation for Isabelle/HOL theories.
You can either import HOL-Library.Code_Binary_Nat, which will use a binary representation for natural numbers instead of a unary one, or you can also import HOL-Library.Code_Target_Nat, where if you are using OCaml, natural numbers will be represented by OCaml's Zarith library.
Notification Bot (Sep 15 2022 at 02:28):Alex Weisberger has marked this topic as unresolved.
Alex Weisberger (Sep 15 2022 at 02:31):I'm running into an error when doing this. I imported "HOL-Library.Code_Target_Nat" and get this error on export_code:
"Nat.zero_nat_inst.zero_nat" is not a constructor, on left hand side of equation, in theorem:
bevalf zero_nat_inst.zero_nat ?t ≡ ?t
In the documentation it says: "Pattern matching with 0 / Suc is eliminated by a preprocessor."
I'm using 0 as a constructor in a function.
Last updated: Apr 19 2024 at 12:27 UTC