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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
