|
Require Import Int63.
Set Implicit Arguments.
Open Scope int63_scope.
Check (eq_refl : 3 -c 2 = C0 1).
Check (eq_refl (C0 1) <: 3 -c 2 = C0 1).
Check (eq_refl (C0 1) <<: 3 -c 2 = C0 1).
Definition compute1 := Eval compute in 3 -c 2.
Check (eq_refl compute1 : C0 1 = C0 1).
Check (eq_refl : 0 -c 1 = C1 9223372036854775807).
Check (eq_refl (C1 9223372036854775807) <: 0 -c 1 = C1 9223372036854775807).
Check (eq_refl (C1 9223372036854775807) <<: 0 -c 1 = C1 9223372036854775807).
Definition compute2 := Eval compute in 0 -c 1.
Check (eq_refl compute2 : C1 9223372036854775807 = C1 9223372036854775807).
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
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.
|
