| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 624 B |
|
Quelle bug_18978.vSprache: Coq |
|||||||||||||||
|
Set Universe Polymorphism. Set Printing Universes. (* Fully explicit definition: we would like to spare the annotation u *) Definition id@{s;u|} (A : Type@{s;u}) (a : A) : A := a. (* Some kind of typical ambiguity can be simulated by rebinding Type to an auxilliary definitio Definition T@{s;u|} := Type@{s;u}. Definition idT@{s;+|} (A : T@{s;_}) (a : A) : A := a. (* The actual problem *) Definition id0@{s;+|} (A : Type@{s;_}) (a : A) : A := a. (* Error: Syntax error: [universe] expected after '|' (in [sort]). *) (* check that we didn't forget the quality annotation *) Check fun (A:SProp) (x:A) => id0 A x.
¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-27