| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/ex/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Code_Timing.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/ex/Code_Timing.thy Author: Florian Haftmann, TU Muenchen, 2016 *) section ‹Examples for code generation timing measures› theory Code_Timing imports "HOL-Number_Theory.Eratosthenes" begin declare [[code_timing]] definition primes_upto :: "nat → int list" where "primes_upto = map int ∘ Eratosthenes.primes_upto" definition "required_symbols _ = (primes_upto, 0 :: nat, Suc, 1 :: nat, numeral :: num → nat, Num.One, Num.Bit0, Num.Bit1, Code_Evaluation.TERM_OF_EQUAL :: int list itself)" ML ‹ val ctxt = context; val consts = [const_name‹required_symbols›]; val simp = Code_Simp.static_conv { ctxt = ctxt, consts = consts, simpset = NONE }; val nbe = Nbe.static_conv { ctxt = ctxt, consts = consts }; ; › ML_val ‹ simp context 🚫‹primes_upto 100› › ML_val ‹ simp context 🚫‹primes_upto 200› › ML_val ‹ nbe context 🚫‹primes_upto 200› › ML_val ‹ nbe context 🚫‹primes_upto 400› › ML_val ‹ nbe context 🚫‹primes_upto 600› › end
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-11