SSL FloatNumberSyntax.v Sprache: Coq

Require Import PrimFloat.

Check 2%float.
Check 2.5%float.
Check (-2.5)%float.
(* Avoid exponents with less than three digits as they are usually
displayed with two digits (1e7 is displayed 1e+07) except on
Windows where three digits are used (1e+007). *)
Check 2.5e123%float.
Check (-2.5e-123)%float.
Check (2 + 2)%float.
Check (2.5 + 2.5)%float.

Open Scope float_scope.

Check 2.
Check 2.5.
Check (-2.5).
Check 2.5e123.
Check (-2.5e-123).
Check (2 + 2).
Check (2.5 + 2.5).
Check -0x1a.
Check 0xb.2c.
Check -0x1ae2.
Check 0xb.2cp2.
Check 0xb.2cp8.
Check -0xb.2cp-2.

Check 1e309.
Check -1e309.

Set Printing All.
Check 0.5.
Unset Printing All.
Check 0.5.
Unset Printing Float.
Check 0.5.
Set Printing Float.
Check 0.5.

Open Scope nat_scope.

Check 2.
Check 2%float.

Delimit Scope float_scope with flt.
Definition t := 2%float.
Print t.
Delimit Scope nat_scope with float.
Print t.
Check 2.
Close Scope nat_scope.
Check 2.
Close Scope float_scope.

quality100%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

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 ist noch experimentell.