| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Word_Lib/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 1 kB |
|
Quelle Hex_Words.thySprache: Isabelle |
|||||||||||||||
|
(* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "Print Words in Hex" theory Hex_Words imports "HOL-Library.Word" begin text ‹Print words in hex.› (* mostly clagged from Num.thy *) typed_print_translation ‹ fun dest_num (Const (@{const_syntax Num.Bit0}, _) $ n) = 2 * dest_num n | dest_num (Const (@{const_syntax Num.Bit1}, _) $ n) = 2 * dest_num n + 1 | dest_num (Const (@{const_syntax Num.One}, _)) = 1; fun dest_bin_hex_str tm = let val num = dest_num tm; val pre = if num < 10 then "" else "0x" in pre ^ (Int.fmt StringCvt.HEX num) end; fun num_tr' sign ctxt T [n] = let val k = dest_bin_hex_str n; val t' = Syntax.const @{syntax_const "_Numeral"} $ Syntax.free (sign ^ k); in case T of Type (@{type_name fun}, [_, T' as Type("Word.word",_)]) => if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t' else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T' | T' => if T' = dummyT then t' else raise Match end; [(@{const_syntax numeral}, num_tr' "")] end › end
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09