|
From Coq Require Import Cyclic31.
Definition Nat `(int31) := nat.
Definition Zero (_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _: digits) := 0.
Check (eq_refl (int31_rect Nat Zero 1) : 0 = 0).
Check (eq_refl (int31_rect Nat Zero 1) <: 0 = 0).
Check (eq_refl (int31_rect Nat Zero 1) <<: 0 = 0).
¤ Dauer der Verarbeitung: 0.15 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.
|
