| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 395 B |
|
Quellcode-Bibliothek bug_3825.vSprache: Coq |
|||||||||||||||
|
Set Universe Polymorphism. Set Printing Universes. Axiom foo@{i j} : Type@{i} -> Type@{j}. Notation bar := foo. Monomorphic Universes i j. Check bar@{i j}. Fail Check bar@{i}. Notation qux := (nat -> nat). Fail Check qux@{i}. Axiom TruncType@{i} : nat -> Type@{i}. Notation "n -Type" := (TruncType n) (at level 1) : type_scope. Notation hProp := (0)-Type. Check hProp. Check hProp@{i}.
¤ 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.11Bemerkung: (vorverarbeitet am 2026-06-04) ¤*Bot Zugriff |
|
||||||||||||||
2026-07-27