section‹Show Implemetation for Real Numbers via Rational Numbers›
text‹We just provide an implementation for show of real numbers where we assume
that real numbers are implemented via rational numbers.›
theory Show_Real_Impl imports
Show_Real
Show_Instances begin
text‹We now define @{const show_real}.› overloading show_real ≡ show_real begin definition show_real where"show_real x ≡ (if (∃ y. x = Ratreal y) then show (THE y. x = Ratreal y) else ''Irrational'')" end
lemma show_real_code[code]: "show_real (Ratreal x) = show x" unfolding show_real_def by auto
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet am 2026-09-29)
¤
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.
