| products/Sources/formale Sprachen/C/Apache/ (Apache Web Server Version 2.4.65©) Datei vom 11.5.2008 mit Größe 4 kB |
|
Quelle Code_Target_Numeral_Float.thy Sprache: Isabelle |
|||||||||||||||
|
(* 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
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-09-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-10