| products/Sources/formale Sprachen/Roqc/test-suite/primitive/uint63/ (Linux Kernel Version 6.17.9©) Datei vom 15.8.2025 mit Größe 667 B |
|
SSL subcarryc.vSprache: Coq |
|||||||||||||||
|
Require Import PrimInt63. Set Implicit Arguments. Open Scope uint63_scope. Check (eq_refl : subcarryc 3 1 = C0 1). Check (eq_refl (C0 1) <: subcarryc 3 1 = C0 1). Check (eq_refl (C0 1) <<: subcarryc 3 1 = C0 1). Definition compute1 := Eval compute in subcarryc 3 1. Check (eq_refl compute1 : C0 1 = C0 1). Check (eq_refl : subcarryc 0 1 = C1 9223372036854775806). Check (eq_refl (C1 9223372036854775806) <: subcarryc 0 1 = C1 9223372036854775806). Check (eq_refl (C1 9223372036854775806) <<: subcarryc 0 1 = C1 9223372036854775806). Definition compute2 := Eval compute in subcarryc 0 1. Check (eq_refl compute2 : C1 9223372036854775806 = C1 9223372036854775806).
¤ 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.0.0Bemerkung: (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09