src/HOL/Library/Code_Target_Numeral_Float.thy
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 73546 7cb3fefef79e
permissions -rw-r--r--
tuned;

(*  Title:      HOL/Library/Code_Target_Numeral_Float.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section \<open>Preprocessor setup for floats implemented by target language numerals\<close>

theory Code_Target_Numeral_Float
imports Float Code_Target_Numeral
begin

lemma numeral_float_computation_unfold [code_computation_unfold]:
  \<open>numeral k = Float (int_of_integer (Code_Numeral.positive k)) 0\<close>
  \<open>- numeral k = Float (int_of_integer (Code_Numeral.negative k)) 0\<close>
  by (simp_all add: Float.compute_float_numeral Float.compute_float_neg_numeral)

end