--- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy Tue Oct 26 14:43:59 2021 +0000
@@ -16,6 +16,14 @@
by a corresponding \<open>export_code\<close> command.
\<close>
+lemma take_bit_num_code [code]: \<comment> \<open>TODO: move\<close>
+ \<open>take_bit_num n m = (case (n, m)
+ of (0, _) \<Rightarrow> None
+ | (Suc n, Num.One) \<Rightarrow> Some Num.One
+ | (Suc n, Num.Bit0 m) \<Rightarrow> (case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))
+ | (Suc n, Num.Bit1 m) \<Rightarrow> Some (case take_bit_num n m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q))\<close>
+ by (cases n; cases m) simp_all
+
export_code _ checking SML OCaml? Haskell? Scala
end