section‹Examples for hexadecimal and binary numerals›
theory Hex_Bin_Examples imports Main begin
text"Hex and bin numerals can be used like normal decimal numerals in input" lemma"0xFF = 255"by (rule refl) lemma"0xF = 0b1111"by (rule refl)
text‹
Just like decimal numeral they are polymorphic, for arithmetic
they need to be constrained › lemma"0x0A + 0x10 = (0x1A :: nat)"by simp
text"The number of leading zeros is irrelevant" lemma"0b00010000 = 0x10"by (rule refl)
text"Unary minus works as for decimal numerals" lemma"- 0x0A = - 10"by (rule refl)
text‹
Hex and bin numerals are printed as decimal: term‹0b10› › term"0b10" term"0x0A"
text‹
The numerals 0 and 1 are syntactically different from the
constants 0 and 1. For the usual numeric types, their values
are the same, though. › lemma"0x01 = 1"oops lemma"0x00 = 0"oops
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.
