Quelle Show_Real_Impl.thy

Sprache: Isabelle

(*
    Author:      René Thiemann
    License:     LGPL
*)

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.9 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.