Theory HOL-Library.Code_Target_Numeral_Float

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

section ‹Preprocessor setup for floats implemented by target language numerals›

theory Code_Target_Numeral_Float
imports Float Code_Target_Numeral
begin

lemma numeral_float_computation_unfold [code_computation_unfold]:
  ‹numeral k = Float (int_of_integer (Code_Numeral.positive k)) 0›
  ‹- numeral k = Float (int_of_integer (Code_Numeral.negative k)) 0›
  by (simp_all add: Float.compute_float_numeral Float.compute_float_neg_numeral)

end