| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/output/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 443 B |
|
Quelle bug_11934.vSprache: Coq |
|||||||||||||||
|
Polymorphic Axiom foo@{u} : Prop -> Prop. Arguments foo {_}. Axiom bla : forall {A B}, @foo A -> @foo B -> Prop. Definition thing := forall (x:@foo@{Type} True) (y:@foo@{Type} True), bla x y. Print thing. (* forall x y : foo, bla x y *) Set Printing Universes. Print thing. (* forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y *) Set Printing Implicit. Print thing. (* BAD: forall x y : @foo@{thing.u0} True, @bla True True x y *)
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09